let x1, x2 be FinSequence of COMPLEX ; ( len x1 = len x2 implies (x1 + x2) *' = (x1 *') + (x2 *') )
reconsider x9 = x1 as Element of (len x1) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9 = x2 as Element of (len x2) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x3 = x1 *' as Element of (len (x1 *')) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x4 = x2 *' as Element of (len (x2 *')) -tuples_on COMPLEX by FINSEQ_2:92;
assume A1:
len x1 = len x2
; (x1 + x2) *' = (x1 *') + (x2 *')
then A2:
len (x1 + x2) = len x1
by Th6;
A3:
( len x1 = len (x1 *') & len x2 = len (x2 *') )
by Def1;
A4:
now for i being Nat st 1 <= i & i <= len ((x1 + x2) *') holds
((x1 + x2) *') . i = (x3 + x4) . ilet i be
Nat;
( 1 <= i & i <= len ((x1 + x2) *') implies ((x1 + x2) *') . i = (x3 + x4) . i )A5:
i in NAT
by ORDINAL1:def 12;
assume that A6:
1
<= i
and A7:
i <= len ((x1 + x2) *')
;
((x1 + x2) *') . i = (x3 + x4) . iA8:
i <= len (x1 + x2)
by A7, Def1;
hence ((x1 + x2) *') . i =
((x1 + x2) . i) *'
by A6, Def1
.=
((x9 . i) + (y9 . i)) *'
by A1, A5, Th14
.=
((x1 . i) *') + ((x2 . i) *')
by COMPLEX1:32
.=
((x1 *') . i) + ((x2 . i) *')
by A2, A6, A8, Def1
.=
((x1 *') . i) + ((x2 *') . i)
by A1, A2, A6, A8, Def1
.=
(x3 + x4) . i
by A1, A3, A5, Th14
;
verum end;
len ((x1 *') + (x2 *')) = len x1
by A1, A3, Th6;
hence
(x1 + x2) *' = (x1 *') + (x2 *')
by A4, A2, Def1; verum