let x, y, z be FinSequence of COMPLEX ; ( len x = len y & len y = len z implies mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) )
assume that
A1:
len x = len y
and
A2:
len y = len z
; mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))
reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on COMPLEX by A1, A2, FINSEQ_2:92;
A3: dom (mlt ((x + y),z)) =
Seg (len (mlt ((x2 + y2),z2)))
by FINSEQ_1:def 3
.=
Seg (len x)
by CARD_1:def 7
.=
Seg (len ((mlt (x2,z2)) + (mlt (y2,z2))))
by CARD_1:def 7
.=
dom ((mlt (x2,z2)) + (mlt (y2,z2)))
by FINSEQ_1:def 3
;
A4: dom (mlt (x,z)) =
Seg (len (mlt (x2,z2)))
by FINSEQ_1:def 3
.=
Seg (len x)
by CARD_1:def 7
.=
Seg (len ((mlt (x2,z2)) + (mlt (y2,z2))))
by CARD_1:def 7
.=
dom ((mlt (x2,z2)) + (mlt (y2,z2)))
by FINSEQ_1:def 3
;
A5: dom (mlt (y,z)) =
Seg (len (mlt (y2,z2)))
by FINSEQ_1:def 3
.=
Seg (len x)
by CARD_1:def 7
.=
Seg (len ((mlt (x2,z2)) + (mlt (y2,z2))))
by CARD_1:def 7
.=
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;
( i in dom (mlt ((x + y),z)) implies (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i )
assume A6:
i in dom (mlt ((x + y),z))
;
(mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i
set a =
x . i;
set b =
y . i;
set d =
(x + y) . i;
set e =
z . i;
len (x2 + y2) = len x
by CARD_1:def 7;
then dom (x2 + y2) =
Seg (len x)
by FINSEQ_1:def 3
.=
Seg (len (mlt (x2,z2)))
by CARD_1:def 7
.=
dom (mlt (x,z))
by FINSEQ_1:def 3
;
then A7:
(x + y) . i = (x . i) + (y . i)
by A3, A4, A6, COMPLSP2:1;
thus (mlt ((x + y),z)) . i =
((x + y) . i) * (z . i)
by A6, Th17
.=
((x . i) * (z . i)) + ((y . i) * (z . i))
by A7
.=
((mlt (x,z)) . i) + ((y . i) * (z . i))
by A3, A4, A6, Th17
.=
((mlt (x,z)) . i) + ((mlt (y,z)) . i)
by A3, A5, A6, Th17
.=
((mlt (x,z)) + (mlt (y,z))) . i
by A3, A6, COMPLSP2:1
;
verum
end;
hence
mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))
by A3, FINSEQ_1:13; verum