let n be Nat; :: thesis: for K being Field
for R being FinSequence_of_Square-Matrix of K holds Det (R | n) = (Det R) | n
let K be Field; :: thesis: for R being FinSequence_of_Square-Matrix of K holds Det (R | n) = (Det R) | n
let R be FinSequence_of_Square-Matrix of K; :: thesis: Det (R | n) = (Det R) | n
A1: len (Det R) = len R by FINSEQ_1:def 18;

per cases ( n >= len R or n < len R ) ;

suppose A2: n >= len R ; :: thesis: Det (R | n) = (Det R) | n

then R | n = R by FINSEQ_1:79;
hence Det (R | n) = (Det R) | n by A1, A2, FINSEQ_1:79; :: thesis: verum

end;

suppose A3: n < len R ; :: thesis: Det (R | n) = (Det R) | n

R = (R | n) ^ (R /^ n) by RFINSEQ:21;
then A4: Det R = (Det (R | n)) ^ (Det (R /^ n)) by Th50;
len (R | n) = n by A3, FINSEQ_1:80;
then len (Det (R | n)) = n by FINSEQ_1:def 18;
hence Det (R | n) = (Det R) | n by A4, FINSEQ_5:26; :: thesis: verum

end;

end;