let n be Nat; :: thesis: for Af being Subset of (n -VectSp_over F_Real)
for Ar being Subset of (REAL-NS n) st Af = Ar holds
[#] (Lin Ar) = [#] (Lin Af)
let Af be Subset of (n -VectSp_over F_Real); :: thesis: for Ar being Subset of (REAL-NS n) st Af = Ar holds
[#] (Lin Ar) = [#] (Lin Af)
let Ar be Subset of (REAL-NS n); :: thesis: ( Af = Ar implies [#] (Lin Ar) = [#] (Lin Af) )
assume A1: Af = Ar ; :: thesis: [#] (Lin Ar) = [#] (Lin Af)
reconsider At = Ar as Subset of (TOP-REAL n) by Th4;
[#] (Lin At) = [#] (Lin Ar) by Th26;
hence [#] (Lin Ar) = [#] (Lin Af) by MATRTOP2:6, A1; :: thesis: verum