let n be Nat; :: thesis: for f1, f2 being n -element complex-valued XFinSequence holds XProduct (f1 (#) f2) = (XProduct f1) * (XProduct f2)
let f1, f2 be n -element complex-valued XFinSequence; :: thesis: XProduct (f1 (#) f2) = (XProduct f1) * (XProduct f2)
defpred S₁[ Nat] means for f1, f2 being $1 -element complex-valued XFinSequence holds XProduct (f1 (#) f2) = (XProduct f1) * (XProduct f2);
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: S₁[k] ; :: thesis: S₁[k + 1]
for f1, f2 being k + 1 -element complex-valued XFinSequence holds XProduct (f1 (#) f2) = (XProduct f1) * (XProduct f2)

proof

let f1, f2 be k + 1 -element complex-valued XFinSequence; :: thesis: XProduct (f1 (#) f2) = (XProduct f1) * (XProduct f2)
reconsider F = f1 (#) f2 as k + 1 -element complex-valued XFinSequence ;
reconsider G = (f1 (#) f2) | k as k -element complex-valued XFinSequence ;
reconsider g1 = f1 | k as k -element complex-valued XFinSequence ;
reconsider g2 = f2 | k as k -element complex-valued XFinSequence ;
C1: ( dom f1 = k + 1 & dom f2 = k + 1 & dom F = k + 1 ) by CARD_1:def 7;
k + 0 < k + 1 by XREAL_1:6;
then C2: ( k in Segm (len f1) & k in Segm (len f2) & k in Segm (len F) ) by C1, NAT_1:44;
then C3: ( XProduct (f1 | (k + 1)) = (XProduct g1) * (f1 . k) & XProduct (f2 | (k + 1)) = (XProduct g2) * (f2 . k) ) by A265;
C4: XProduct (g1 (#) g2) = (XProduct g1) * (XProduct g2) by B1;
XProduct F = XProduct (F | (k + 1))
.= (XProduct G) * (F . k) by C2, A265
.= ((XProduct g1) * (XProduct g2)) * ((f1 (#) f2) . k) by C4, MFG
.= ((XProduct g1) * (XProduct g2)) * ((f1 . k) * (f2 . k)) by C2, VALUED_1:def 4
.= (XProduct f1) * (XProduct f2) by C3 ;
hence XProduct (f1 (#) f2) = (XProduct f1) * (XProduct f2) ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A2: S₁[ 0 ]

proof

let f1, f2 be 0 -element complex-valued XFinSequence; :: thesis: XProduct (f1 (#) f2) = (XProduct f1) * (XProduct f2)
( XProduct (f1 (#) f2) = 1 & XProduct f1 = 1 & XProduct f2 = 1 ) by PFO;
hence XProduct (f1 (#) f2) = (XProduct f1) * (XProduct f2) ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A1);
hence XProduct (f1 (#) f2) = (XProduct f1) * (XProduct f2) ; :: thesis: verum