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 (R1 ^ R2) = (len R1) + (len R2) by FINSEQ_1:22;
A2: len ((Det R1) ^ (Det R2)) = (len R1) + (len R2) by CARD_1:def 7;
len R2 = len (Det R2) by CARD_1:def 7;
then A3: dom (Det R2) = dom R2 by FINSEQ_3:29;
A4: len R1 = len (Det R1) by CARD_1:def 7;
then A5: dom (Det R1) = dom R1 by FINSEQ_3:29;
A6: len (Det (R1 ^ R2)) = len (R1 ^ R2) by CARD_1:def 7;
then A7: dom ((Det R1) ^ (Det R2)) = dom (Det (R1 ^ R2)) by A1, A2, FINSEQ_3:29;

now :: thesis: for k being Nat st 1 <= k & k <= (len R1) + (len R2) holds
(Det (R1 ^ R2)) . k = ((Det R1) ^ (Det R2)) . k

let k be Nat; :: thesis: ( 1 <= k & k <= (len R1) + (len R2) implies (Det (R1 ^ R2)) . k = ((Det R1) ^ (Det R2)) . k )
assume that
A8: 1 <= k and
A9: k <= (len R1) + (len R2) ; :: thesis: (Det (R1 ^ R2)) . k = ((Det R1) ^ (Det R2)) . k
A10: k in dom ((Det R1) ^ (Det R2)) by A2, A8, A9, FINSEQ_3:25;

now :: thesis: ((Det R1) ^ (Det R2)) . k = (Det (R1 ^ R2)) . k

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

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

then A12: len (R1 . k) = len ((R1 ^ R2) . k) by A5, FINSEQ_1:def 7;
thus ((Det R1) ^ (Det R2)) . k = (Det R1) . k by A11, FINSEQ_1:def 7
.= Det (R1 . k) by A11, Def7
.= Det ((R1 ^ R2) . k) by A5, A11, A12, FINSEQ_1:def 7
.= (Det (R1 ^ R2)) . k by A7, A10, 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
A13: n in dom (Det R2) and
A14: k = (len R1) + n by A4;
A15: len (R2 . n) = len ((R1 ^ R2) . k) by A3, A13, A14, FINSEQ_1:def 7;
thus ((Det R1) ^ (Det R2)) . k = (Det R2) . n by A4, A13, A14, FINSEQ_1:def 7
.= Det (R2 . n) by A13, Def7
.= Det ((R1 ^ R2) . k) by A3, A13, A14, A15, FINSEQ_1:def 7
.= (Det (R1 ^ R2)) . k by A7, A10, 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 A6, A1, A2; :: thesis: verum