let K be Field; :: thesis: for G, G1 being FinSequence_of_Matrix of K
for p, p1 being FinSequence of K st len G = len p & len G1 <= len p1 holds
mlt (p ^ p1),(G ^ G1) = (mlt p,G) ^ (mlt p1,G1)
let G, G1 be FinSequence_of_Matrix of K; :: thesis: for p, p1 being FinSequence of K st len G = len p & len G1 <= len p1 holds
mlt (p ^ p1),(G ^ G1) = (mlt p,G) ^ (mlt p1,G1)
let p, p1 be FinSequence of K; :: thesis: ( len G = len p & len G1 <= len p1 implies mlt (p ^ p1),(G ^ G1) = (mlt p,G) ^ (mlt p1,G1) )
assume that
A1: len G = len p and
A2: len G1 <= len p1 ; :: thesis: mlt (p ^ p1),(G ^ G1) = (mlt p,G) ^ (mlt p1,G1)
A3: dom G = dom p by A1, FINSEQ_3:31;
dom G1 = Seg (len G1) by FINSEQ_1:def 3;
then dom G1 c= Seg (len p1) by A2, FINSEQ_1:7;
then A4: dom G1 c= dom p1 by FINSEQ_1:def 3;
set M1 = mlt p1,G1;
set M = mlt p,G;
set GG1 = G ^ G1;
set pp1 = p ^ p1;
set MM = mlt (p ^ p1),(G ^ G1);
A5: dom (G ^ G1) = Seg (len (G ^ G1)) by FINSEQ_1:def 3;
A6: dom (mlt (p ^ p1),(G ^ G1)) = dom (G ^ G1) by Def9;
A7: dom (mlt p1,G1) = dom G1 by Def9;
then A8: len (mlt p1,G1) = len G1 by FINSEQ_3:31;
A9: dom (mlt p,G) = dom G by Def9;
then A10: len (mlt p,G) = len G by FINSEQ_3:31;
len (G ^ G1) = (len G) + (len G1) by FINSEQ_1:35;
then len (G ^ G1) <= (len p) + (len p1) by A1, A2, XREAL_1:9;
then dom (G ^ G1) c= Seg ((len p) + (len p1)) by A5, FINSEQ_1:7;
then A11: dom (G ^ G1) c= dom (p ^ p1) by FINSEQ_1:def 7;

A12: now

let i be Nat; :: thesis: ( 1 <= i & i <= len (G ^ G1) implies (mlt (p ^ p1),(G ^ G1)) . i = ((mlt p,G) ^ (mlt p1,G1)) . i )
assume that
A13: 1 <= i and
A14: i <= len (G ^ G1) ; :: thesis: (mlt (p ^ p1),(G ^ G1)) . i = ((mlt p,G) ^ (mlt p1,G1)) . i
A15: i in dom (G ^ G1) by A13, A14, FINSEQ_3:27;
then A16: (p ^ p1) /. i = (p ^ p1) . i by A11, PARTFUN1:def 8;
A17: (mlt (p ^ p1),(G ^ G1)) . i = ((p ^ p1) /. i) * ((G ^ G1) . i) by A6, A15, Def9;

now

per cases ( i in dom G or ex n being Nat st
( n in dom G1 & i = (len G) + n ) ) by A15, FINSEQ_1:38;

suppose A18: i in dom G ; :: thesis: (mlt (p ^ p1),(G ^ G1)) . i = ((mlt p,G) ^ (mlt p1,G1)) . i

then A19: (G ^ G1) . i = G . i by FINSEQ_1:def 7;
A20: p . i = p /. i by A3, A18, PARTFUN1:def 8;
(p ^ p1) . i = p . i by A3, A18, FINSEQ_1:def 7;
hence (mlt (p ^ p1),(G ^ G1)) . i = (mlt p,G) . i by A9, A17, A16, A18, A19, A20, Def9
.= ((mlt p,G) ^ (mlt p1,G1)) . i by A9, A18, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom G1 & i = (len G) + n ) ; :: thesis: (mlt (p ^ p1),(G ^ G1)) . i = ((mlt p,G) ^ (mlt p1,G1)) . i

then consider n being Nat such that
A21: n in dom G1 and
A22: i = (len G) + n ;
A23: (G ^ G1) . i = G1 . n by A21, A22, FINSEQ_1:def 7;
A24: p1 /. n = p1 . n by A4, A21, PARTFUN1:def 8;
(p ^ p1) . i = p1 . n by A1, A4, A21, A22, FINSEQ_1:def 7;
hence (mlt (p ^ p1),(G ^ G1)) . i = (mlt p1,G1) . n by A7, A17, A16, A21, A23, A24, Def9
.= ((mlt p,G) ^ (mlt p1,G1)) . i by A7, A10, A21, A22, FINSEQ_1:def 7 ;
:: thesis: verum

end;

end;

end;

hence (mlt (p ^ p1),(G ^ G1)) . i = ((mlt p,G) ^ (mlt p1,G1)) . i ; :: thesis: verum

end;

A25: len ((mlt p,G) ^ (mlt p1,G1)) = (len (mlt p,G)) + (len (mlt p1,G1)) by FINSEQ_1:35;
len (mlt (p ^ p1),(G ^ G1)) = len (G ^ G1) by A6, FINSEQ_3:31;
hence mlt (p ^ p1),(G ^ G1) = (mlt p,G) ^ (mlt p1,G1) by A10, A8, A25, A12, FINSEQ_1:18, FINSEQ_1:35; :: thesis: verum