let V1, V2 be free finite-rank Z_Module; :: thesis: for b2, b3 being OrdBasis of V2
for f being bilinear-FrForm of V1,V2
for v1 being Vector of V1
for v2 being Vector of V2
for X, Y being FinSequence of F_Real st len X = len b2 & len Y = len b2 & ( for k being Nat st k in Seg (len b2) holds
Y . k = f . (v1,(b2 /. k)) ) & X = v2 |-- b2 holds
Y "*" X = f . (v1,v2)
let b2, b3 be OrdBasis of V2; :: thesis: for f being bilinear-FrForm of V1,V2
for v1 being Vector of V1
for v2 being Vector of V2
for X, Y being FinSequence of F_Real st len X = len b2 & len Y = len b2 & ( for k being Nat st k in Seg (len b2) holds
Y . k = f . (v1,(b2 /. k)) ) & X = v2 |-- b2 holds
Y "*" X = f . (v1,v2)
let f be bilinear-FrForm of V1,V2; :: thesis: for v1 being Vector of V1
for v2 being Vector of V2
for X, Y being FinSequence of F_Real st len X = len b2 & len Y = len b2 & ( for k being Nat st k in Seg (len b2) holds
Y . k = f . (v1,(b2 /. k)) ) & X = v2 |-- b2 holds
Y "*" X = f . (v1,v2)
let v1 be Vector of V1; :: thesis: for v2 being Vector of V2
for X, Y being FinSequence of F_Real st len X = len b2 & len Y = len b2 & ( for k being Nat st k in Seg (len b2) holds
Y . k = f . (v1,(b2 /. k)) ) & X = v2 |-- b2 holds
Y "*" X = f . (v1,v2)
let v2 be Vector of V2; :: thesis: for X, Y being FinSequence of F_Real st len X = len b2 & len Y = len b2 & ( for k being Nat st k in Seg (len b2) holds
Y . k = f . (v1,(b2 /. k)) ) & X = v2 |-- b2 holds
Y "*" X = f . (v1,v2)
let X, Y be FinSequence of F_Real; :: thesis: ( len X = len b2 & len Y = len b2 & ( for k being Nat st k in Seg (len b2) holds
Y . k = f . (v1,(b2 /. k)) ) & X = v2 |-- b2 implies Y "*" X = f . (v1,v2) )
assume that
A1: len X = len b2 and
A2: len Y = len b2 and
A3: for k being Nat st k in Seg (len b2) holds
Y . k = f . (v1,(b2 /. k)) and
A4: X = v2 |-- b2 ; :: thesis: Y "*" X = f . (v1,v2)
set x = v2 |-- b2;
P2: for k being Nat st k in Seg (len (v2 |-- b2)) holds
Y . k = (FrFunctionalFAF (f,v1)) . (b2 /. k)

proof

let k be Nat; :: thesis: ( k in Seg (len (v2 |-- b2)) implies Y . k = (FrFunctionalFAF (f,v1)) . (b2 /. k) )
assume k in Seg (len (v2 |-- b2)) ; :: thesis: Y . k = (FrFunctionalFAF (f,v1)) . (b2 /. k)
then Y . k = f . (v1,(b2 /. k)) by A1, A3, A4;
hence Y . k = (FrFunctionalFAF (f,v1)) . (b2 /. k) by HTh8; :: thesis: verum

end;

thus Y "*" X = X "*" Y by FVSUM_1:90
.= (FrFunctionalFAF (f,v1)) . (Sum (lmlt ((v2 |-- b2),b2))) by LMThMBF1X0, A1, A2, A4, P2
.= f . (v1,(Sum (lmlt ((v2 |-- b2),b2)))) by HTh8
.= f . (v1,v2) by ZMATRLIN:30 ; :: thesis: verum