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 n >= len R ; :: thesis: Det (R | n) = (Det R) | n

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

end;

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

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

end;

end;