let K be Field; :: thesis: for x, y, z being FinSequence of K st len x = len y & len y = len z holds
mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))

let x, y, z be FinSequence of K; :: thesis: ( 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 ; :: thesis: mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))
A3: dom z = Seg (len x) by ;
reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on the carrier of K by ;
A4: dom (x + y) = Seg (len (x2 + y2)) by FINSEQ_1:def 3
.= Seg (len x) by CARD_1:def 7
.= dom z by ;
A5: dom (mlt (y,z)) = Seg (len (mlt (y2,z2))) by FINSEQ_1:def 3
.= Seg (len x) by CARD_1:def 7 ;
then A6: dom (mlt (y,z)) = 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 ;
A7: dom x = Seg (len x) by FINSEQ_1:def 3;
A8: dom y = Seg (len x) by ;
A9: dom (mlt (x,z)) = Seg (len (mlt (x2,z2))) by FINSEQ_1:def 3
.= Seg (len x) by CARD_1:def 7 ;
then A10: dom (mlt (x,z)) = 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 ;
A11: 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 )
A12: ( rng x c= the carrier of K & rng y c= the carrier of K ) by FINSEQ_1:def 4;
A13: ( rng z c= the carrier of K & rng (x + y) c= the carrier of K ) by FINSEQ_1:def 4;
dom the multF of K = [: the carrier of K, the carrier of K:] by FUNCT_2:def 1;
then ( mlt ((x + y),z) = the multF of K .: ((x + y),z) & [:(rng (x + y)),(rng z):] c= dom the multF of K ) by ;
then A14: dom (mlt ((x + y),z)) = (dom (x + y)) /\ (dom z) by FUNCOP_1:69;
assume A15: i in dom (mlt ((x + y),z)) ; :: thesis: (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i
then i in dom z by ;
then A16: z . i in rng z by FUNCT_1:def 3;
len (x2 + y2) = len x by CARD_1:def 7;
then A17: dom (x2 + y2) = Seg (len x) by FINSEQ_1:def 3;
then A18: i in Seg (len x) by ;
then A19: (x + y) . i in rng (x + y) by ;
i in dom y by ;
then A20: y . i in rng y by FUNCT_1:def 3;
A21: i in dom x by ;
then x . i in rng x by FUNCT_1:def 3;
then reconsider a = x . i, b = y . i, d = (x + y) . i, e = z . i as Element of K by A12, A13, A20, A16, A19;
dom <:y,z:> = (dom x) /\ (dom x) by
.= dom x ;
then A22: i in dom <:y,z:> by ;
dom [:y,z:] = [:(dom y),(dom z):] by FUNCT_3:def 8;
then A23: [i,i] in dom [:y,z:] by ;
dom [:y,z:] = [:(dom y),(dom z):] by FUNCT_3:def 8;
then A24: [i,i] in dom [:y,z:] by ;
dom the multF of K = [: the carrier of K, the carrier of K:] by FUNCT_2:def 1;
then [b,e] in dom the multF of K by ZFMISC_1:87;
then ( dom ( the multF of K * (y,z)) = dom ( the multF of K * [:y,z:]) & [:y,z:] . (i,i) in dom the multF of K ) by ;
then [i,i] in dom ( the multF of K * (y,z)) by ;
then A25: b * e = ( the multF of K * (y,z)) . (i,i) by FINSEQOP:77
.= ( the multF of K * [:y,z:]) . (i,i) by FINSEQOP:def 4
.= the multF of K . ([:y,z:] . (i,i)) by
.= the multF of K . ((y . i),(z . i)) by
.= the multF of K . (<:y,z:> . i) by
.= ( the multF of K * <:y,z:>) . i by
.= ( the multF of K .: (y,z)) . i by FUNCOP_1:def 3
.= (mlt (y,z)) . i by FVSUM_1:def 7 ;
dom <:(x + y),z:> = (dom (x + y)) /\ (dom z) by FUNCT_3:def 7
.= dom x by ;
then A26: i in dom <:(x + y),z:> by ;
A27: (mlt ((x + y),z)) . i = ( the multF of K .: ((x + y),z)) . i by FVSUM_1:def 7
.= ( the multF of K * <:(x + y),z:>) . i by FUNCOP_1:def 3
.= the multF of K . (<:(x + y),z:> . i) by
.= d * e by ;
A28: dom <:(mlt (x,z)),(mlt (y,z)):> = (dom (mlt (x,z))) /\ (dom (mlt (y,z))) by FUNCT_3:def 7
.= dom x by ;
A29: dom <:x,y:> = (dom x) /\ (dom y) by FUNCT_3:def 7
.= dom x by A8, A7 ;
A30: the addF of K .: ((mlt (x,z)),(mlt (y,z))) = (mlt (x,z)) + (mlt (y,z)) by FVSUM_1:def 3;
dom [:x,z:] = [:(dom x),(dom z):] by FUNCT_3:def 8;
then A31: [i,i] in dom [:x,z:] by ;
dom [:x,z:] = [:(dom x),(dom z):] by FUNCT_3:def 8;
then A32: [i,i] in dom [:x,z:] by ;
dom <:x,z:> = (dom x) /\ (dom x) by
.= dom x ;
then A33: i in dom <:x,z:> by ;
A34: (x + y) . i = ( the addF of K .: (x,y)) . i by FVSUM_1:def 3
.= ( the addF of K * <:x,y:>) . i by FUNCOP_1:def 3
.= the addF of K . (<:x,y:> . i) by
.= a + b by ;
dom the multF of K = [: the carrier of K, the carrier of K:] by FUNCT_2:def 1;
then [a,e] in dom the multF of K by ZFMISC_1:87;
then ( dom ( the multF of K * (x,z)) = dom ( the multF of K * [:x,z:]) & [:x,z:] . (i,i) in dom the multF of K ) by ;
then [i,i] in dom ( the multF of K * (x,z)) by ;
then a * e = ( the multF of K * (x,z)) . (i,i) by FINSEQOP:77
.= ( the multF of K * [:x,z:]) . (i,i) by FINSEQOP:def 4
.= the multF of K . ([:x,z:] . (i,i)) by
.= the multF of K . ((x . i),(z . i)) by
.= the multF of K . (<:x,z:> . i) by
.= ( the multF of K * <:x,z:>) . i by
.= ( the multF of K .: (x,z)) . i by FUNCOP_1:def 3
.= (mlt (x,z)) . i by FVSUM_1:def 7 ;
then (a * e) + (b * e) = the addF of K . (<:(mlt (x,z)),(mlt (y,z)):> . i) by
.= ( the addF of K * <:(mlt (x,z)),(mlt (y,z)):>) . i by
.= ((mlt (x,z)) + (mlt (y,z))) . i by ;
hence (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i by ; :: thesis: verum
end;
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 ;
hence mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) by ; :: thesis: verum