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

proof

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

end;

thus X "*" Y = (FrFunctionalSAF (f,v2)) . (Sum (lmlt ((v1 |-- b1),b1))) by LMThMBF1X0, A1, A2, A4, P2
.= f . ((Sum (lmlt ((v1 |-- b1),b1))),v2) by HTh9
.= f . (v1,v2) by ZMATRLIN:30 ; :: thesis: verum