let K be Field; :: thesis: for R1, R2 being FinSequence_of_Square-Matrix of K holds Det (R1 ^ R2) = (Det R1) ^ (Det R2)
let R1, R2 be FinSequence_of_Square-Matrix of K; :: thesis: Det (R1 ^ R2) = (Det R1) ^ (Det R2)
set R12 = R1 ^ R2;
A1: ( len (Det (R1 ^ R2)) = len (R1 ^ R2) & len (R1 ^ R2) = (len R1) + (len R2) & len R1 = len (Det R1) & len R2 = len (Det R2) ) by FINSEQ_1:35, FINSEQ_1:def 18;
then A2: len ((Det R1) ^ (Det R2)) = (len R1) + (len R2) by FINSEQ_1:35;
then A3: ( dom (Det R1) = dom R1 & dom (Det R2) = dom R2 & dom ((Det R1) ^ (Det R2)) = dom (Det (R1 ^ R2)) ) by A1, FINSEQ_3:31;

now

let k be Nat; :: thesis: ( 1 <= k & k <= (len R1) + (len R2) implies (Det (R1 ^ R2)) . k = ((Det R1) ^ (Det R2)) . k )
assume A4: ( 1 <= k & k <= (len R1) + (len R2) ) ; :: thesis: (Det (R1 ^ R2)) . k = ((Det R1) ^ (Det R2)) . k
A5: k in dom ((Det R1) ^ (Det R2)) by A2, A4, FINSEQ_3:27;

now

per cases ( k in dom (Det R1) or ex n being Nat st
( n in dom (Det R2) & k = (len (Det R1)) + n ) ) by A5, FINSEQ_1:38;

suppose A6: k in dom (Det R1) ; :: thesis: ((Det R1) ^ (Det R2)) . k = (Det (R1 ^ R2)) . k

A7: len (R1 . k) = len ((R1 ^ R2) . k) by A3, A6, FINSEQ_1:def 7;
thus ((Det R1) ^ (Det R2)) . k = (Det R1) . k by A6, FINSEQ_1:def 7
.= Det (R1 . k) by A6, Def7
.= Det ((R1 ^ R2) . k) by A3, A6, A7, FINSEQ_1:def 7
.= (Det (R1 ^ R2)) . k by A3, A5, Def7 ; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom (Det R2) & k = (len (Det R1)) + n ) ; :: thesis: ((Det R1) ^ (Det R2)) . k = (Det (R1 ^ R2)) . k

then consider n being Nat such that
A8: ( n in dom (Det R2) & k = (len R1) + n ) by A1;
A9: len (R2 . n) = len ((R1 ^ R2) . k) by A3, A8, FINSEQ_1:def 7;
thus ((Det R1) ^ (Det R2)) . k = (Det R2) . n by A1, A8, FINSEQ_1:def 7
.= Det (R2 . n) by A8, Def7
.= Det ((R1 ^ R2) . k) by A9, A3, A8, FINSEQ_1:def 7
.= (Det (R1 ^ R2)) . k by A3, A5, Def7 ; :: thesis: verum

end;

end;

end;

hence (Det (R1 ^ R2)) . k = ((Det R1) ^ (Det R2)) . k ; :: thesis: verum

end;

hence Det (R1 ^ R2) = (Det R1) ^ (Det R2) by A1, A2, FINSEQ_1:18; :: thesis: verum