let f be FinSequence of E ^omega ; :: thesis: f is XFinSequence-yielding
let x be set ; :: according to REWRITE2:def 1 :: thesis: ( x in dom f implies f . x is XFinSequence )
assume A1: x in dom f ; :: thesis: f . x is XFinSequence
then reconsider x = x as Nat ;
f . x in E ^omega by A1, FINSEQ_2:11;
hence f . x is XFinSequence ; :: thesis: verum