let f be FinSequence of NAT ; :: thesis: f is Cardinal-yielding
let x be set ; :: according to CARD_3:def 1 :: thesis: ( not x in proj1 f or f . x is set )
assume x in dom f ; :: thesis: f . x is set
thus f . x is set ; :: thesis: verum