let n be Nat; :: thesis: for D being non empty set
for F1 being FinSequence_of_Matrix of D holds Len (F1 | n) = (Len F1) | n
let D be non empty set ; :: thesis: for F1 being FinSequence_of_Matrix of D holds Len (F1 | n) = (Len F1) | n
let F1 be FinSequence_of_Matrix of D; :: thesis: Len (F1 | n) = (Len F1) | n
A1: len (Len F1) = len F1 by CARD_1:def 7;

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

suppose A2: n >= len F1 ; :: thesis: Len (F1 | n) = (Len F1) | n

then F1 | n = F1 by FINSEQ_1:58;
hence Len (F1 | n) = (Len F1) | n by A1, A2, FINSEQ_1:58; :: thesis: verum

end;

suppose A3: n < len F1 ; :: thesis: Len (F1 | n) = (Len F1) | n

F1 = (F1 | n) ^ (F1 /^ n) by RFINSEQ:8;
then A4: Len F1 = (Len (F1 | n)) ^ (Len (F1 /^ n)) by Th14;
len (F1 | n) = n by A3, FINSEQ_1:59;
then len (Len (F1 | n)) = n by CARD_1:def 7;
hence Len (F1 | n) = (Len F1) | n by A4, FINSEQ_5:23; :: thesis: verum

end;

end;