Je n'ai pas vraiment écrit, mais il me semble que ça devrait marcher... Je commence par extraire une famille libre maximale des
(bizarre d'appeler
et
des vecteurs...), puis je lui fais un coup de Gram-Schmidt pour l'orthonormaliser... Il me semble que ton hypothèse (c'est ça que je n'ai pas eu la patience d'expliciter) entraine que les mêmes opérations appliquées aux
d'indices assortis, me fabrique une famille orthonormale extraite des
(ce qui prouve déjà que les deux systèmes sont de même rang). Je peux toujours envoyer les premiers sur les seconds... Ensuite les coordonnées des
restants sur les
de la base, s'exprimant avec des produits scalaires, et pareil pour les
garantit que ça se prolonge automatiquement à ceux-ci. Reste à prolonger par 0 sur un supplémentaire du sous-espace engendré par les
.