let G be non empty multLoopStr ; :: thesis:
let x1, x2, y1, y2 be FinSequence of G; :: thesis:
assume A1: ( len x1 = len x2 & len y1 = len y2 ) ; :: thesis:
A3: the multF of G .: (x1 ^ y1),(x2 ^ y2) = the multF of G * <:(x1 ^ y1),(x2 ^ y2):> by FUNCOP_1:def 3;
A4: dom the multF of G = [:the carrier of G,the carrier of G:] by FUNCT_2:def 1;
A5: rng (x1 ^ y1) c= the carrier of G by FINSEQ_1:def 4;
B4c: rng (x2 ^ y2) c= the carrier of G by FINSEQ_1:def 4;
B4b: [:(rng (x1 ^ y1)),(rng (x2 ^ y2)):] c= dom the multF of G by A5, A4, B4c, ZFMISC_1:119;
B4a: dom (the multF of G * <:(x1 ^ y1),(x2 ^ y2):>) = (dom (x1 ^ y1)) /\ (dom (x2 ^ y2)) by A3, B4b, FUNCOP_1:84;
B5: len (x1 ^ y1) = (len x1) + (len y1) by FINSEQ_1:35;
B6: len (x2 ^ y2) = (len x2) + (len y2) by FINSEQ_1:35;
B7: dom (x1 ^ y1) = Seg (len (x1 ^ y1)) by FINSEQ_1:def 3;
D1: dom (x2 ^ y2) = Seg (len (x2 ^ y2)) by FINSEQ_1:def 3;
D2: dom (x1 ^ y1) = dom (x2 ^ y2) by A1, B6, B7, D1, FINSEQ_1:35;
B10: dom (mlt (x1 ^ y1),(x2 ^ y2)) = dom (x1 ^ y1) by A3, B4a, D2, FVSUM_1:def 7;
A8: len (mlt (x1 ^ y1),(x2 ^ y2)) = len (x1 ^ y1) by B7, B10, FINSEQ_1:def 3
.= (len x1) + (len y1) by FINSEQ_1:35 ;
C5: dom x2 = Seg (len x1) by A1, FINSEQ_1:def 3
.= dom x1 by FINSEQ_1:def 3 ;
C5b: dom y2 = Seg (len y1) by A1, FINSEQ_1:def 3
.= dom y1 by FINSEQ_1:def 3 ;
A3: the multF of G .: x1,x2 = the multF of G * <:x1,x2:> by FUNCOP_1:def 3;
A4: dom the multF of G = [:the carrier of G,the carrier of G:] by FUNCT_2:def 1;
A5: rng x1 c= the carrier of G by FINSEQ_1:def 4;
B12: rng x2 c= the carrier of G by FINSEQ_1:def 4;
B13: [:(rng x1),(rng x2):] c= dom the multF of G by A5, A4, B12, ZFMISC_1:119;
B14: dom (the multF of G * <:x1,x2:>) = (dom x1) /\ (dom x2) by A3, B13, FUNCOP_1:84;
C8: dom (mlt x1,x2) = dom x1 by C5, A3, B14, FVSUM_1:def 7;
B16: dom (mlt x1,x2) = Seg (len x1) by C8, FINSEQ_1:def 3;
A3: the multF of G .: y1,y2 = the multF of G * <:y1,y2:> by FUNCOP_1:def 3;
A5: rng y1 c= the carrier of G by FINSEQ_1:def 4;
B18: rng y2 c= the carrier of G by FINSEQ_1:def 4;
B19: [:(rng y1),(rng y2):] c= dom the multF of G by A5, A4, B18, ZFMISC_1:119;
B20: dom (the multF of G * <:y1,y2:>) = (dom y1) /\ (dom y2) by A3, B19, FUNCOP_1:84;
C8b: dom (mlt y1,y2) = dom y1 by C5b, A3, B20, FVSUM_1:def 7;
B21: dom (mlt y1,y2) = Seg (len y1) by C8b, FINSEQ_1:def 3;
B23: len (mlt y1,y2) = len y1 by B21, FINSEQ_1:def 3;
B24: len (mlt (x1 ^ y1),(x2 ^ y2)) = (len (mlt x1,x2)) + (len (mlt y1,y2)) by A8, B16, B23, FINSEQ_1:def 3;
A2: len (mlt (x1 ^ y1),(x2 ^ y2)) = len ((mlt x1,x2) ^ (mlt y1,y2)) by B24, FINSEQ_1:35;
for i being Nat st 1 <= i & i <= len (mlt (x1 ^ y1),(x2 ^ y2)) holds
(mlt (x1 ^ y1),(x2 ^ y2)) . i = ((mlt x1,x2) ^ (mlt y1,y2)) . i

proof

let i be Nat; :: thesis:
assume B1: ( 1 <= i & i <= len (mlt (x1 ^ y1),(x2 ^ y2)) ) ; :: thesis:
B2: i in Seg (len (mlt (x1 ^ y1),(x2 ^ y2))) by B1, FINSEQ_1:3;
B3: i in dom (mlt (x1 ^ y1),(x2 ^ y2)) by B2, FINSEQ_1:def 3;
B22: ( 1 <= i & i <= (len x1) + (len y1) ) by B3, B7, B5, B10, FINSEQ_1:3;
K2: i <= len (x1 ^ y1) by B3, B7, B10, FINSEQ_1:3;
A36: (x1 ^ y1) /. i = (x1 ^ y1) . i by B1, K2, FINSEQ_4:24;
A36a: i <= len (x2 ^ y2) by B3, B7, B5, B10, B6, A1, FINSEQ_1:3;
A37: (x2 ^ y2) /. i = (x2 ^ y2) . i by B1, A36a, FINSEQ_4:24;

now

per cases ;

suppose C0: i <= len x1 ; :: thesis:

then C2: i in Seg (len x1) by B1, FINSEQ_1:3;
C1: i in dom x1 by C2, FINSEQ_1:def 3;
A34: x1 /. i = x1 . i by B1, C0, FINSEQ_4:24;
A35: x2 /. i = x2 . i by B1, C0, A1, FINSEQ_4:24;
K2: i in dom x2 by C2, A1, FINSEQ_1:def 3;
C4: (x2 ^ y2) . i = x2 . i by K2, FINSEQ_1:def 7;
C7: i in dom (mlt x1,x2) by C2, C8, FINSEQ_1:def 3;
((mlt x1,x2) ^ (mlt y1,y2)) . i = (mlt x1,x2) . i by C7, FINSEQ_1:def 7
.= (x1 /. i) * (x2 /. i) by C7, FV73 ;
hence ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt x1,x2) ^ (mlt y1,y2)) . i by C1, C4, A34, A35, A36, A37, FINSEQ_1:def 7; :: thesis:

end;

suppose C0: i > len x1 ; :: thesis:

set k = i -' (len x1);
C11: i -' (len x1) = i - (len x1) by C0, XREAL_1:235;
C2: i = (len x1) + (i -' (len x1)) by C11;
C2a: i -' (len x1) > 0 by C0, C11, XREAL_1:52;
C12: 0 + 1 <= i -' (len x1) by C2a, NAT_1:13;
C12a: i - (len x1) <= ((len x1) + (len y1)) - (len x1) by B22, XREAL_1:15;
C56: i -' (len x1) <= len y1 by C0, C12a, XREAL_1:235;
C10: i -' (len x1) in Seg (len y1) by C12, C56, FINSEQ_1:3;
C10a: i -' (len x1) in dom y2 by A1, C10, FINSEQ_1:def 3;
C4a: i -' (len x1) in Seg (len y1) by C12, C56, FINSEQ_1:3;
C13: i -' (len x1) in dom y1 by C4a, FINSEQ_1:def 3;
C3: (x1 ^ y1) . i = y1 . (i -' (len x1)) by C2, C13, FINSEQ_1:def 7;
C7: i -' (len x1) in dom (mlt y1,y2) by C8b, C4a, FINSEQ_1:def 3;
A34: y1 /. (i -' (len x1)) = y1 . (i -' (len x1)) by C56, C12, FINSEQ_4:24;
A35: y2 /. (i -' (len x1)) = y2 . (i -' (len x1)) by C56, C12, A1, FINSEQ_4:24;
K2: i <= len (x1 ^ y1) by B3, B7, B10, FINSEQ_1:3;
A36: (x1 ^ y1) /. i = (x1 ^ y1) . i by B1, K2, FINSEQ_4:24;
A36a: i <= len (x2 ^ y2) by B3, B7, B5, B10, B6, A1, FINSEQ_1:3;
A37: (x2 ^ y2) /. i = (x2 ^ y2) . i by B1, A36a, FINSEQ_4:24;
A37a: i = (len (mlt x1,x2)) + (i -' (len x1)) by B16, C2, FINSEQ_1:def 3;
((mlt x1,x2) ^ (mlt y1,y2)) . i = (mlt y1,y2) . (i -' (len x1)) by C7, A37a, FINSEQ_1:def 7
.= (y1 /. (i -' (len x1))) * (y2 /. (i -' (len x1))) by C7, FV73 ;
hence ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt x1,x2) ^ (mlt y1,y2)) . i by C3, C2, A1, C10a, A34, A35, A36, A37, FINSEQ_1:def 7; :: thesis:

end;

hence (mlt (x1 ^ y1),(x2 ^ y2)) . i = ((mlt x1,x2) ^ (mlt y1,y2)) . i by B3, FV73; :: thesis:

end;

hence mlt (x1 ^ y1),(x2 ^ y2) = (mlt x1,x2) ^ (mlt y1,y2) by A2, FINSEQ_1:18; :: thesis: