set mc = multcomplex ;
consider f being FinSequence of COMPLEX such that
A1:
f = F
and
A2:
Product F = multcomplex $$ f
by Def13;
set g = [#] (f,(the_unity_wrt multcomplex));
defpred S1[ Nat] means multcomplex $$ ((finSeg F),([#] (f,(the_unity_wrt multcomplex)))) is real ;
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is
real
then reconsider a =
([#] (f,(the_unity_wrt multcomplex))) . (k + 1),
b =
multcomplex $$ (
(finSeg k),
([#] (f,(the_unity_wrt multcomplex)))) as
Real by A4;
not
k + 1
in Seg k
by FINSEQ_3:8;
then multcomplex $$ (
((finSeg k) \/ {.(In ((k + 1),NAT)).}),
([#] (f,(the_unity_wrt multcomplex)))) =
multcomplex . (
(multcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt multcomplex))))),
(([#] (f,(the_unity_wrt multcomplex))) . (k + 1)))
by SETWOP_2:2
.=
b * a
by BINOP_2:def 5
;
hence
S1[
k + 1]
by FINSEQ_1:9;
verum
end;
A5:
( multcomplex $$ f = multcomplex $$ ((findom f),([#] (f,(the_unity_wrt multcomplex)))) & ex n being Nat st dom f = Seg n )
by FINSEQ_1:def 2, SETWOP_2:def 2;
Seg 0 = {}. NAT
;
then A6:
S1[ 0 ]
by BINOP_2:6, SETWISEO:31;
for n being Nat holds S1[n]
from NAT_1:sch 2(A6, A3);
hence
Product F is real
by A2, A5; verum