let K be Field; :: thesis: for G, G', G1, G2 being FinSequence_of_Matrix of K st len G = len G' holds
(G ^ G1) (#) (G' ^ G2) = (G (#) G') ^ (G1 (#) G2)
let G, G', G1, G2 be FinSequence_of_Matrix of K; :: thesis: ( len G = len G' implies (G ^ G1) (#) (G' ^ G2) = (G (#) G') ^ (G1 (#) G2) )
assume A1: len G = len G' ; :: thesis: (G ^ G1) (#) (G' ^ G2) = (G (#) G') ^ (G1 (#) G2)
set GG' = G (#) G';
set G12 = G1 (#) G2;
set GG1 = G ^ G1;
set GG2 = G' ^ G2;
A2: ( dom (G (#) G') = dom G & dom (G1 (#) G2) = dom G1 & dom ((G ^ G1) (#) (G' ^ G2)) = dom (G ^ G1) & dom G = dom G' ) by A1, Def11, FINSEQ_3:31;
then A3: ( len (G (#) G') = len G & len (G1 (#) G2) = len G1 & len ((G ^ G1) (#) (G' ^ G2)) = len (G ^ G1) ) by FINSEQ_3:31;
A4: ( len (G ^ G1) = (len G) + (len G1) & len (G' ^ G2) = (len G) + (len G2) ) by A1, FINSEQ_1:35;
then A5: ( len ((G ^ G1) (#) (G' ^ G2)) = len ((G (#) G') ^ (G1 (#) G2)) & len ((G (#) G') ^ (G1 (#) G2)) = (len (G (#) G')) + (len (G1 (#) G2)) ) by A3, FINSEQ_1:35;

now

let i be Nat; :: thesis: ( 1 <= i & i <= (len G) + (len G1) implies ((G ^ G1) (#) (G' ^ G2)) . i = ((G (#) G') ^ (G1 (#) G2)) . i )
assume A6: ( 1 <= i & i <= (len G) + (len G1) ) ; :: thesis: ((G ^ G1) (#) (G' ^ G2)) . i = ((G (#) G') ^ (G1 (#) G2)) . i
A7: i in dom ((G ^ G1) (#) (G' ^ G2)) by A2, A4, A6, FINSEQ_3:27;
then A8: ((G ^ G1) (#) (G' ^ G2)) . i = ((G ^ G1) . i) * ((G' ^ G2) . i) by Def11;

now

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

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

hence ((G ^ G1) (#) (G' ^ G2)) . i = (G . i) * ((G' ^ G2) . i) by A8, FINSEQ_1:def 7
.= (G . i) * (G' . i) by A2, A9, FINSEQ_1:def 7
.= (G (#) G') . i by A2, A9, Def11
.= ((G (#) G') ^ (G1 (#) G2)) . i by A2, A9, FINSEQ_1:def 7 ;
:: thesis: verum

end;

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

then consider n being Nat such that
A10: ( n in dom G1 & i = (len G) + n ) ;

now

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

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

hence (G' ^ G2) . i = G2 . n by A1, A10, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A11: not n in dom G2 ; :: thesis: (G' ^ G2) . i = G2 . n

then ( ( n < 1 or n > len G2 ) & 1 <= n ) by A10, FINSEQ_3:27;
then i > (len G) + (len G2) by A10, XREAL_1:10;
then not i in dom (G' ^ G2) by A4, FINSEQ_3:27;
hence (G' ^ G2) . i = {} by FUNCT_1:def 4
.= G2 . n by A11, FUNCT_1:def 4 ;
:: thesis: verum

end;

end;

end;

hence ((G ^ G1) (#) (G' ^ G2)) . i = (G1 . n) * (G2 . n) by A8, A10, FINSEQ_1:def 7
.= (G1 (#) G2) . n by A2, A10, Def11
.= ((G (#) G') ^ (G1 (#) G2)) . i by A2, A3, A10, FINSEQ_1:def 7 ;
:: thesis: verum

end;

end;

end;

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

end;

hence (G ^ G1) (#) (G' ^ G2) = (G (#) G') ^ (G1 (#) G2) by A3, A5, FINSEQ_1:18; :: thesis: verum