now

let i be Nat; :: thesis: ( i in dom (F | n) implies (F | n) . i is Matrix of D )
assume A1: i in dom (F | n) ; :: thesis: (F | n) . i is Matrix of D
(F | n) . i = F . i by A1, FUNCT_1:70;
hence (F | n) . i is Matrix of D ; :: thesis: verum

end;

hence F | n is FinSequence_of_Matrix of D by Def2; :: thesis: verum