let x, y, z be FinSequence of COMPLEX ; :: thesis: ( len x = len y & len y = len z implies mlt (x + y),z = (mlt x,z) + (mlt y,z) )
assume
( len x = len y & len y = len z )
; :: thesis: mlt (x + y),z = (mlt x,z) + (mlt y,z)
then reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:110;
A1: dom (mlt (x + y),z) =
Seg (len (mlt (x2 + y2),z2))
by FINSEQ_1:def 3
.=
Seg (len x)
by FINSEQ_1:def 18
.=
Seg (len ((mlt x2,z2) + (mlt y2,z2)))
by FINSEQ_1:def 18
.=
dom ((mlt x2,z2) + (mlt y2,z2))
by FINSEQ_1:def 3
;
A2: dom (mlt x,z) =
Seg (len (mlt x2,z2))
by FINSEQ_1:def 3
.=
Seg (len x)
by FINSEQ_1:def 18
.=
Seg (len ((mlt x2,z2) + (mlt y2,z2)))
by FINSEQ_1:def 18
.=
dom ((mlt x2,z2) + (mlt y2,z2))
by FINSEQ_1:def 3
;
A3: dom (mlt y,z) =
Seg (len (mlt y2,z2))
by FINSEQ_1:def 3
.=
Seg (len x)
by FINSEQ_1:def 18
.=
Seg (len ((mlt x2,z2) + (mlt y2,z2)))
by FINSEQ_1:def 18
.=
dom ((mlt x2,z2) + (mlt y2,z2))
by FINSEQ_1:def 3
;
for i being Nat st i in dom (mlt (x + y),z) holds
(mlt (x + y),z) . i = ((mlt x,z) + (mlt y,z)) . i
proof
let i be
Nat;
:: thesis: ( i in dom (mlt (x + y),z) implies (mlt (x + y),z) . i = ((mlt x,z) + (mlt y,z)) . i )
assume A4:
i in dom (mlt (x + y),z)
;
:: thesis: (mlt (x + y),z) . i = ((mlt x,z) + (mlt y,z)) . i
len (x2 + y2) = len x
by FINSEQ_1:def 18;
then A5:
dom (x2 + y2) =
Seg (len x)
by FINSEQ_1:def 3
.=
Seg (len (mlt x2,z2))
by FINSEQ_1:def 18
.=
dom (mlt x,z)
by FINSEQ_1:def 3
;
set a =
x . i;
set b =
y . i;
set d =
(x + y) . i;
set e =
z . i;
A6:
(x + y) . i = (x . i) + (y . i)
by A1, A2, A4, A5, COMPLSP2:1;
thus (mlt (x + y),z) . i =
((x + y) . i) * (z . i)
by A4, Th19
.=
((x . i) * (z . i)) + ((y . i) * (z . i))
by A6
.=
((mlt x,z) . i) + ((y . i) * (z . i))
by A1, A2, A4, Th19
.=
((mlt x,z) . i) + ((mlt y,z) . i)
by A1, A3, A4, Th19
.=
((mlt x,z) + (mlt y,z)) . i
by A1, A4, COMPLSP2:1
;
:: thesis: verum
end;
hence
mlt (x + y),z = (mlt x,z) + (mlt y,z)
by A1, FINSEQ_1:17; :: thesis: verum