reconsider FC = F_Complex , FR = F_Real as Field ;
defpred S₁[ Nat] means for fc being FinSequence of FC
for fr being FinSequence of FR st fc = fr & len fc = $1 holds
Product fc = Product fr;
A1: S₁[ 0 ]

proof

let fc be FinSequence of FC; :: thesis: for fr being FinSequence of FR st fc = fr & len fc = 0 holds
Product fc = Product fr
let fr be FinSequence of FR; :: thesis: ( fc = fr & len fc = 0 implies Product fc = Product fr )
assume A2: ( fc = fr & len fc = 0 ) ; :: thesis: Product fc = Product fr
A3: ( fc = <*> the carrier of FC & fr = fc & fc = <*> the carrier of FR ) by A2;
hence Product fc = 1_ FR by COMPLEX1:def 4, COMPLFLD:8, GROUP_4:8
.= Product fr by A3, GROUP_4:8 ;
:: thesis: verum

end;

A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let fc be FinSequence of FC; :: thesis: for fr being FinSequence of FR st fc = fr & len fc = n + 1 holds
Product fc = Product fr
let fr be FinSequence of FR; :: thesis: ( fc = fr & len fc = n + 1 implies Product fc = Product fr )
assume A6: ( fc = fr & len fc = n + 1 ) ; :: thesis: Product fc = Product fr
reconsider x = Product (fr | n), y = fr /. (n + 1) as Real ;
n < n + 1 by NAT_1:13;
then A7: ( len (fc | n) = n & n = len (fr | n) ) by A6, FINSEQ_1:59;
1 <= n + 1 by NAT_1:11;
then A8: ( fc /. (n + 1) = fc . (n + 1) & fc . (n + 1) = fr /. (n + 1) ) by A6, PARTFUN1:def 6, FINSEQ_3:25;
A9: ( fr = (fr | n) ^ <*(fr /. (n + 1))*> & fc = (fc | n) ^ <*(fc /. (n + 1))*> ) by A6, FINSEQ_5:21;
hence Product fc = (Product (fc | n)) * (fc /. (n + 1)) by GROUP_4:6
.= multcomplex . ((Product (fc | n)),(fc /. (n + 1))) by COMPLFLD:def 1
.= multcomplex . (x,y) by A5, A6, A7, A8
.= x * y by BINOP_2:def 5
.= (Product (fr | n)) * (fr /. (n + 1)) by BINOP_2:def 11
.= Product fr by A9, GROUP_4:6 ;
:: thesis: verum

end;

let fc be FinSequence of F_Complex; :: thesis: for fr being FinSequence of F_Real st fc = fr holds
Product fc = Product fr
let fr be FinSequence of F_Real; :: thesis: ( fc = fr implies Product fc = Product fr )
assume A10: fc = fr ; :: thesis: Product fc = Product fr
for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A4);
then S₁[ len fc] ;
hence Product fc = Product fr by A10; :: thesis: verum