let D be set ; :: thesis: for n being Nat
for r being set st r in D holds
n --> r is XFinSequence of
let n be Nat; :: thesis: for r being set st r in D holds
n --> r is XFinSequence of
let r be set ; :: thesis: ( r in D implies n --> r is XFinSequence of )
assume A1: r in D ; :: thesis: n --> r is XFinSequence of
reconsider p = n --> r as XFinSequence by Th3;

now

per cases ( n <> 0 or n = 0 ) ;

case n <> 0 ; :: thesis: n --> r is XFinSequence of

then A2: rng p = {r} by FUNCOP_1:14;
rng p c= D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in D )
assume x in rng p ; :: thesis: x in D
hence x in D by A1, A2, TARSKI:def 1; :: thesis: verum

end;

hence n --> r is XFinSequence of by RELAT_1:def 19; :: thesis: verum

end;

case n = 0 ; :: thesis: n --> r is XFinSequence of

then len p = 0 by FUNCOP_1:16;
then n --> r = {} by AFINSQ_1:18;
hence n --> r is XFinSequence of by AFINSQ_1:19; :: thesis: verum

end;

end;

end;

hence n --> r is XFinSequence of ; :: thesis: verum