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 FINSEQ_1:def 18;

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

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

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

end;

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

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

end;

end;