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 A1: ( len G = len p & len G1 <= len p1 ) ; :: thesis: mlt (p ^ p1),(G ^ G1) = (mlt p,G) ^ (mlt p1,G1)
set pp1 = p ^ p1;
set GG1 = G ^ G1;
set MM = mlt (p ^ p1),(G ^ G1);
set M = mlt p,G;
set M1 = mlt p1,G1;
A2: ( dom (mlt (p ^ p1),(G ^ G1)) = dom (G ^ G1) & dom (mlt p,G) = dom G & dom (mlt p1,G1) = dom G1 & dom G = dom p & dom (G ^ G1) = Seg (len (G ^ G1)) & dom G1 = Seg (len G1) ) by A1, Def9, FINSEQ_1:def 3, FINSEQ_3:31;
then A3: ( len (mlt (p ^ p1),(G ^ G1)) = len (G ^ G1) & len (mlt p,G) = len G & len (mlt p1,G1) = len G1 & len (G ^ G1) = (len G) + (len G1) & len ((mlt p,G) ^ (mlt p1,G1)) = (len (mlt p,G)) + (len (mlt p1,G1)) ) by FINSEQ_1:35, FINSEQ_3:31;
then len (G ^ G1) <= (len p) + (len p1) by A1, XREAL_1:9;
then ( dom (G ^ G1) c= Seg ((len p) + (len p1)) & dom G1 c= Seg (len p1) ) by A1, A2, FINSEQ_1:7;
then A4: ( dom (G ^ G1) c= dom (p ^ p1) & dom G1 c= dom p1 ) by FINSEQ_1:def 3, FINSEQ_1:def 7;

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 A5: ( 1 <= i & i <= len (G ^ G1) ) ; :: thesis: (mlt (p ^ p1),(G ^ G1)) . i = ((mlt p,G) ^ (mlt p1,G1)) . i
A6: i in dom (G ^ G1) by A5, FINSEQ_3:27;
then A7: ( (mlt (p ^ p1),(G ^ G1)) . i = ((p ^ p1) /. i) * ((G ^ G1) . i) & (p ^ p1) /. i = (p ^ p1) . i ) by A2, A4, Def9, PARTFUN1:def 8;

now

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

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

then ( (G ^ G1) . i = G . i & (p ^ p1) . i = p . i & p . i = p /. i ) by A2, FINSEQ_1:def 7, PARTFUN1:def 8;
hence (mlt (p ^ p1),(G ^ G1)) . i = (mlt p,G) . i by A2, A7, A8, Def9
.= ((mlt p,G) ^ (mlt p1,G1)) . i by A2, A8, 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
A9: ( n in dom G1 & i = (len G) + n ) ;
( (G ^ G1) . i = G1 . n & (p ^ p1) . i = p1 . n & p1 /. n = p1 . n ) by A1, A4, A9, FINSEQ_1:def 7, PARTFUN1:def 8;
hence (mlt (p ^ p1),(G ^ G1)) . i = (mlt p1,G1) . n by A2, A7, A9, Def9
.= ((mlt p,G) ^ (mlt p1,G1)) . i by A2, A3, A9, 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;

hence mlt (p ^ p1),(G ^ G1) = (mlt p,G) ^ (mlt p1,G1) by A3, FINSEQ_1:18; :: thesis: verum