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

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