let K be Field; :: thesis: for G, G9, G1, G2 being FinSequence_of_Matrix of K st len G = len G9 holds
(G ^ G1) (#) (G9 ^ G2) = (G (#) G9) ^ (G1 (#) G2)
let G, G9, G1, G2 be FinSequence_of_Matrix of K; :: thesis: ( len G = len G9 implies (G ^ G1) (#) (G9 ^ G2) = (G (#) G9) ^ (G1 (#) G2) )
set GG9 = G (#) G9;
set G12 = G1 (#) G2;
set GG1 = G ^ G1;
set GG2 = G9 ^ G2;
A1: len (G ^ G1) = (len G) + (len G1) by FINSEQ_1:22;
A2: dom (G (#) G9) = dom G by Def11;
then A3: len (G (#) G9) = len G by FINSEQ_3:29;
A4: dom ((G ^ G1) (#) (G9 ^ G2)) = dom (G ^ G1) by Def11;
then A5: len ((G ^ G1) (#) (G9 ^ G2)) = len (G ^ G1) by FINSEQ_3:29;
assume A6: len G = len G9 ; :: thesis: (G ^ G1) (#) (G9 ^ G2) = (G (#) G9) ^ (G1 (#) G2)
then A7: len (G9 ^ G2) = (len G) + (len G2) by FINSEQ_1:22;
A8: len ((G (#) G9) ^ (G1 (#) G2)) = (len (G (#) G9)) + (len (G1 (#) G2)) by FINSEQ_1:22;
A9: dom (G1 (#) G2) = dom G1 by Def11;
A10: dom G = dom G9 by A6, FINSEQ_3:29;

A11: now :: thesis: for i being Nat st 1 <= i & i <= (len G) + (len G1) holds
((G ^ G1) (#) (G9 ^ G2)) . i = ((G (#) G9) ^ (G1 (#) G2)) . i

let i be Nat; :: thesis: ( 1 <= i & i <= (len G) + (len G1) implies ((G ^ G1) (#) (G9 ^ G2)) . i = ((G (#) G9) ^ (G1 (#) G2)) . i )
assume that
A12: 1 <= i and
A13: i <= (len G) + (len G1) ; :: thesis: ((G ^ G1) (#) (G9 ^ G2)) . i = ((G (#) G9) ^ (G1 (#) G2)) . i
A14: i in dom ((G ^ G1) (#) (G9 ^ G2)) by A4, A1, A12, A13, FINSEQ_3:25;
then A15: ((G ^ G1) (#) (G9 ^ G2)) . i = ((G ^ G1) . i) * ((G9 ^ G2) . i) by Def11;

now :: thesis: ((G ^ G1) (#) (G9 ^ G2)) . i = ((G (#) G9) ^ (G1 (#) G2)) . i

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

suppose A16: i in dom G ; :: thesis: ((G ^ G1) (#) (G9 ^ G2)) . i = ((G (#) G9) ^ (G1 (#) G2)) . i

hence ((G ^ G1) (#) (G9 ^ G2)) . i = (G . i) * ((G9 ^ G2) . i) by A15, FINSEQ_1:def 7
.= (G . i) * (G9 . i) by A10, A16, FINSEQ_1:def 7
.= (G (#) G9) . i by A2, A16, Def11
.= ((G (#) G9) ^ (G1 (#) G2)) . i by A2, A16, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom G1 & i = (len G) + n ) ; :: thesis: ((G ^ G1) (#) (G9 ^ G2)) . i = ((G (#) G9) ^ (G1 (#) G2)) . i

then consider n being Nat such that
A17: n in dom G1 and
A18: i = (len G) + n ;

now :: thesis: (G9 ^ G2) . i = G2 . n

per cases ( n in dom G2 or not n in dom G2 ) ;

suppose n in dom G2 ; :: thesis: (G9 ^ G2) . i = G2 . n

hence (G9 ^ G2) . i = G2 . n by A6, A18, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A19: not n in dom G2 ; :: thesis: (G9 ^ G2) . i = G2 . n

then ( n < 1 or n > len G2 ) by FINSEQ_3:25;
then i > (len G) + (len G2) by A17, A18, FINSEQ_3:25, XREAL_1:8;
then not i in dom (G9 ^ G2) by A7, FINSEQ_3:25;
hence (G9 ^ G2) . i = {} by FUNCT_1:def 2
.= G2 . n by A19, FUNCT_1:def 2 ;
:: thesis: verum

end;

end;

end;

hence ((G ^ G1) (#) (G9 ^ G2)) . i = (G1 . n) * (G2 . n) by A15, A17, A18, FINSEQ_1:def 7
.= (G1 (#) G2) . n by A9, A17, Def11
.= ((G (#) G9) ^ (G1 (#) G2)) . i by A9, A3, A17, A18, FINSEQ_1:def 7 ;
:: thesis: verum

end;

end;

end;

hence ((G ^ G1) (#) (G9 ^ G2)) . i = ((G (#) G9) ^ (G1 (#) G2)) . i ; :: thesis: verum

end;

len (G1 (#) G2) = len G1 by A9, FINSEQ_3:29;
hence (G ^ G1) (#) (G9 ^ G2) = (G (#) G9) ^ (G1 (#) G2) by A3, A5, A1, A8, A11; :: thesis: verum