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