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:29;
dom G1 = Seg (len G1) by FINSEQ_1:def 3;
then dom G1 c= Seg (len p1) by A2, FINSEQ_1:5;
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:29;
A9: dom (mlt (p,G)) = dom G by Def9;
then A10: len (mlt (p,G)) = len G by FINSEQ_3:29;
len (G ^ G1) = (len G) + (len G1) by FINSEQ_1:22;
then len (G ^ G1) <= (len p) + (len p1) by A1, A2, XREAL_1:7;
then dom (G ^ G1) c= Seg ((len p) + (len p1)) by A5, FINSEQ_1:5;
then A11: dom (G ^ G1) c= dom (p ^ p1) by FINSEQ_1:def 7;

A12: now :: thesis: for i being Nat st 1 <= i & i <= len (G ^ G1) holds
(mlt ((p ^ p1),(G ^ G1))) . i = ((mlt (p,G)) ^ (mlt (p1,G1))) . i

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:25;
then A16: (p ^ p1) /. i = (p ^ p1) . i by A11, PARTFUN1:def 6;
A17: (mlt ((p ^ p1),(G ^ G1))) . i = ((p ^ p1) /. i) * ((G ^ G1) . i) by A6, A15, Def9;

now :: thesis: (mlt ((p ^ p1),(G ^ G1))) . i = ((mlt (p,G)) ^ (mlt (p1,G1))) . i

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

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 6;
(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 6;
(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:22;
len (mlt ((p ^ p1),(G ^ G1))) = len (G ^ G1) by A6, FINSEQ_3:29;
hence mlt ((p ^ p1),(G ^ G1)) = (mlt (p,G)) ^ (mlt (p1,G1)) by A10, A8, A25, A12, FINSEQ_1:22; :: thesis: verum