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 A1, A2, FINSEQ_1:def 3;

reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on the carrier of K by A1, A2, FINSEQ_2:92;

A4: dom (x + y) = Seg (len (x2 + y2)) by FINSEQ_1:def 3

.= Seg (len x) by CARD_1:def 7

.= dom z by A1, A2, 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 ;

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 A1, FINSEQ_1:def 3;

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

.= 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 A11, FINSEQ_1:13; :: thesis: verum

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 A1, A2, FINSEQ_1:def 3;

reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on the carrier of K by A1, A2, FINSEQ_2:92;

A4: dom (x + y) = Seg (len (x2 + y2)) by FINSEQ_1:def 3

.= Seg (len x) by CARD_1:def 7

.= dom z by A1, A2, 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 ;

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 A1, FINSEQ_1:def 3;

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

dom (mlt ((x + y),z)) =
Seg (len (mlt ((x2 + y2),z2)))
by FINSEQ_1:def 3
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 A13, FVSUM_1:def 7, ZFMISC_1:96;

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 A14, XBOOLE_0:def 4;

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 A15, A14, XBOOLE_0:def 4;

then A19: (x + y) . i in rng (x + y) by A17, FUNCT_1:def 3;

i in dom y by A1, A18, FINSEQ_1:def 3;

then A20: y . i in rng y by FUNCT_1:def 3;

A21: i in dom x by A18, FINSEQ_1:def 3;

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 A8, A3, A7, FUNCT_3:def 7

.= dom x ;

then A22: i in dom <:y,z:> by A18, FINSEQ_1:def 3;

dom [:y,z:] = [:(dom y),(dom z):] by FUNCT_3:def 8;

then A23: [i,i] in dom [:y,z:] by A8, A3, A15, A17, A14, ZFMISC_1:87;

dom [:y,z:] = [:(dom y),(dom z):] by FUNCT_3:def 8;

then A24: [i,i] in dom [:y,z:] by A8, A3, A15, A17, A14, ZFMISC_1:87;

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 A8, A3, A15, A17, A14, FINSEQOP:def 4, FUNCT_3:def 8;

then [i,i] in dom ( the multF of K * (y,z)) by A24, FUNCT_1:11;

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 A23, FUNCT_1:13

.= the multF of K . ((y . i),(z . i)) by A8, A3, A15, A17, A14, FUNCT_3:def 8

.= the multF of K . (<:y,z:> . i) by A8, A3, A15, A17, A14, FUNCT_3:49

.= ( the multF of K * <:y,z:>) . i by A22, FUNCT_1:13

.= ( 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 A3, A4, FINSEQ_1:def 3 ;

then A26: i in dom <:(x + y),z:> by A18, FINSEQ_1:def 3;

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 A26, FUNCT_1:13

.= d * e by A4, A15, A14, FUNCT_3:49 ;

A28: dom <:(mlt (x,z)),(mlt (y,z)):> = (dom (mlt (x,z))) /\ (dom (mlt (y,z))) by FUNCT_3:def 7

.= dom x by A9, A5, FINSEQ_1:def 3 ;

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 A3, A7, A15, A17, A14, ZFMISC_1:87;

dom [:x,z:] = [:(dom x),(dom z):] by FUNCT_3:def 8;

then A32: [i,i] in dom [:x,z:] by A3, A7, A15, A17, A14, ZFMISC_1:87;

dom <:x,z:> = (dom x) /\ (dom x) by A3, A7, FUNCT_3:def 7

.= dom x ;

then A33: i in dom <:x,z:> by A18, FINSEQ_1:def 3;

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 A21, A29, FUNCT_1:13

.= a + b by A8, A7, A18, FUNCT_3:49 ;

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 A3, A7, A15, A17, A14, FINSEQOP:def 4, FUNCT_3:def 8;

then [i,i] in dom ( the multF of K * (x,z)) by A32, FUNCT_1:11;

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 A31, FUNCT_1:13

.= the multF of K . ((x . i),(z . i)) by A3, A7, A15, A17, A14, FUNCT_3:def 8

.= the multF of K . (<:x,z:> . i) by A3, A7, A15, A17, A14, FUNCT_3:49

.= ( the multF of K * <:x,z:>) . i by A33, FUNCT_1:13

.= ( 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 A9, A10, A6, A18, A25, FUNCT_3:49

.= ( the addF of K * <:(mlt (x,z)),(mlt (y,z)):>) . i by A21, A28, FUNCT_1:13

.= ((mlt (x,z)) + (mlt (y,z))) . i by A30, FUNCOP_1:def 3 ;

hence (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i by A34, A27, VECTSP_1:def 7; :: thesis: verum

end;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 A13, FVSUM_1:def 7, ZFMISC_1:96;

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 A14, XBOOLE_0:def 4;

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 A15, A14, XBOOLE_0:def 4;

then A19: (x + y) . i in rng (x + y) by A17, FUNCT_1:def 3;

i in dom y by A1, A18, FINSEQ_1:def 3;

then A20: y . i in rng y by FUNCT_1:def 3;

A21: i in dom x by A18, FINSEQ_1:def 3;

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 A8, A3, A7, FUNCT_3:def 7

.= dom x ;

then A22: i in dom <:y,z:> by A18, FINSEQ_1:def 3;

dom [:y,z:] = [:(dom y),(dom z):] by FUNCT_3:def 8;

then A23: [i,i] in dom [:y,z:] by A8, A3, A15, A17, A14, ZFMISC_1:87;

dom [:y,z:] = [:(dom y),(dom z):] by FUNCT_3:def 8;

then A24: [i,i] in dom [:y,z:] by A8, A3, A15, A17, A14, ZFMISC_1:87;

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 A8, A3, A15, A17, A14, FINSEQOP:def 4, FUNCT_3:def 8;

then [i,i] in dom ( the multF of K * (y,z)) by A24, FUNCT_1:11;

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 A23, FUNCT_1:13

.= the multF of K . ((y . i),(z . i)) by A8, A3, A15, A17, A14, FUNCT_3:def 8

.= the multF of K . (<:y,z:> . i) by A8, A3, A15, A17, A14, FUNCT_3:49

.= ( the multF of K * <:y,z:>) . i by A22, FUNCT_1:13

.= ( 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 A3, A4, FINSEQ_1:def 3 ;

then A26: i in dom <:(x + y),z:> by A18, FINSEQ_1:def 3;

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 A26, FUNCT_1:13

.= d * e by A4, A15, A14, FUNCT_3:49 ;

A28: dom <:(mlt (x,z)),(mlt (y,z)):> = (dom (mlt (x,z))) /\ (dom (mlt (y,z))) by FUNCT_3:def 7

.= dom x by A9, A5, FINSEQ_1:def 3 ;

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 A3, A7, A15, A17, A14, ZFMISC_1:87;

dom [:x,z:] = [:(dom x),(dom z):] by FUNCT_3:def 8;

then A32: [i,i] in dom [:x,z:] by A3, A7, A15, A17, A14, ZFMISC_1:87;

dom <:x,z:> = (dom x) /\ (dom x) by A3, A7, FUNCT_3:def 7

.= dom x ;

then A33: i in dom <:x,z:> by A18, FINSEQ_1:def 3;

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 A21, A29, FUNCT_1:13

.= a + b by A8, A7, A18, FUNCT_3:49 ;

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 A3, A7, A15, A17, A14, FINSEQOP:def 4, FUNCT_3:def 8;

then [i,i] in dom ( the multF of K * (x,z)) by A32, FUNCT_1:11;

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 A31, FUNCT_1:13

.= the multF of K . ((x . i),(z . i)) by A3, A7, A15, A17, A14, FUNCT_3:def 8

.= the multF of K . (<:x,z:> . i) by A3, A7, A15, A17, A14, FUNCT_3:49

.= ( the multF of K * <:x,z:>) . i by A33, FUNCT_1:13

.= ( 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 A9, A10, A6, A18, A25, FUNCT_3:49

.= ( the addF of K * <:(mlt (x,z)),(mlt (y,z)):>) . i by A21, A28, FUNCT_1:13

.= ((mlt (x,z)) + (mlt (y,z))) . i by A30, FUNCOP_1:def 3 ;

hence (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i by A34, A27, VECTSP_1:def 7; :: thesis: verum

.= 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 A11, FINSEQ_1:13; :: thesis: verum