now :: thesis: for i being Nat st i in dom (F | n) holds
(F | n) . i is Matrix of D

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

end;

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