let x1, x2 be FinSequence of COMPLEX ; :: thesis: ( 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 ; :: thesis: (x1 - x2) *' = (x1 *') - (x2 *')

then A2: len (x1 - x2) = len x1 by Th7;

A3: ( len x1 = len (x1 *') & len x2 = len (x2 *') ) by Def1;

hence (x1 - x2) *' = (x1 *') - (x2 *') by A4, A2, Def1; :: thesis: verum

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 ; :: thesis: (x1 - x2) *' = (x1 *') - (x2 *')

then A2: len (x1 - x2) = len x1 by Th7;

A3: ( len x1 = len (x1 *') & len x2 = len (x2 *') ) by Def1;

A4: now :: thesis: for i being Nat st 1 <= i & i <= len ((x1 - x2) *') holds

((x1 - x2) *') . i = (x3 - x4) . i

len ((x1 *') - (x2 *')) = len x1
by A1, A3, Th7;((x1 - x2) *') . i = (x3 - x4) . i

let i be Nat; :: thesis: ( 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) *') ; :: thesis: ((x1 - x2) *') . i = (x3 - x4) . i

A8: i <= len (x1 - x2) by A7, Def1;

hence ((x1 - x2) *') . i = ((x1 - x2) . i) *' by A6, Def1

.= ((x9 . i) - (y9 . i)) *' by A1, A5, Th16

.= ((x1 . i) *') - ((x2 . i) *') by COMPLEX1:34

.= ((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, Th16 ;

:: thesis: verum

end;A5: i in NAT by ORDINAL1:def 12;

assume that

A6: 1 <= i and

A7: i <= len ((x1 - x2) *') ; :: thesis: ((x1 - x2) *') . i = (x3 - x4) . i

A8: i <= len (x1 - x2) by A7, Def1;

hence ((x1 - x2) *') . i = ((x1 - x2) . i) *' by A6, Def1

.= ((x9 . i) - (y9 . i)) *' by A1, A5, Th16

.= ((x1 . i) *') - ((x2 . i) *') by COMPLEX1:34

.= ((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, Th16 ;

:: thesis: verum

hence (x1 - x2) *' = (x1 *') - (x2 *') by A4, A2, Def1; :: thesis: verum