let n be Nat; :: thesis: for D being non empty set
for F1 being FinSequence_of_Matrix of D holds Width (F1 | n) = (Width F1) | n
let D be non empty set ; :: thesis: for F1 being FinSequence_of_Matrix of D holds Width (F1 | n) = (Width F1) | n
let F1 be FinSequence_of_Matrix of D; :: thesis: Width (F1 | n) = (Width F1) | n
A1: len (Width F1) = len F1 by CARD_1:def 7;
per cases ( n >= len F1 or n < len F1 ) ;
suppose A2: n >= len F1 ; :: thesis: Width (F1 | n) = (Width F1) | n
then F1 | n = F1 by FINSEQ_1:58;
hence Width (F1 | n) = (Width F1) | n by A1, A2, FINSEQ_1:58; :: thesis: verum
end;
suppose A3: n < len F1 ; :: thesis: Width (F1 | n) = (Width F1) | n
F1 = (F1 | n) ^ (F1 /^ n) by RFINSEQ:8;
then A4: Width F1 = (Width (F1 | n)) ^ (Width (F1 /^ n)) by Th18;
len (F1 | n) = n by A3, FINSEQ_1:59;
then len (Width (F1 | n)) = n by CARD_1:def 7;
hence Width (F1 | n) = (Width F1) | n by A4, FINSEQ_5:23; :: thesis: verum
end;
end;