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 CARD_1:def 7;
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:58;
hence Det (R | n) = (Det R) | n by A1, A2, FINSEQ_1:58; :: thesis: verum
end;
suppose A3: n < len R ; :: thesis: Det (R | n) = (Det R) | n
R = (R | n) ^ (R /^ n) by RFINSEQ:8;
then A4: Det R = (Det (R | n)) ^ (Det (R /^ n)) by Th50;
len (R | n) = n by A3, FINSEQ_1:59;
then len (Det (R | n)) = n by CARD_1:def 7;
hence Det (R | n) = (Det R) | n by A4, FINSEQ_5:23; :: thesis: verum
end;
end;