let x be set ; :: thesis: for A being FinSequence st x in rng A holds
( A <- x in dom A & x = A . (A <- x) )
let A be FinSequence; :: thesis: ( x in rng A implies ( A <- x in dom A & x = A . (A <- x) ) )
assume x in rng A ; :: thesis: ( A <- x in dom A & x = A . (A <- x) )
then A " {x} <> {} by FUNCT_1:72;
then consider y being object such that
A1: y in A " {x} by XBOOLE_0:def 1;
A2: A " {x} c= dom A by RELAT_1:132;
then y in dom A by A1;
then reconsider y = y as Element of NAT ;
defpred S₁[ Nat] means $1 in A " {x};
y = y ;
then A3: ex n being Nat st S₁[n] by A1;
consider n being Nat such that
A4: ( S₁[n] & ( for m being Nat st S₁[m] holds
n <= m ) ) from NAT_1:sch 5(A3);
A5: A <- x c= n by A4, SETFAM_1:3;
for z being set st z in A " {x} holds
Segm n c= z

proof

let z be set ; :: thesis: ( z in A " {x} implies Segm n c= z )
assume A6: z in A " {x} ; :: thesis: Segm n c= z
then z in dom A by A2;
then reconsider z = z as Element of NAT ;
S₁[z] by A6;
then n <= z by A4;
then Segm n c= Segm z by NAT_1:39;
hence Segm n c= z ; :: thesis: verum

end;

then n c= A <- x by A1, SETFAM_1:5;
then A7: A <- x = n by A5;
hence A <- x in dom A by A4, FUNCT_1:def 7; :: thesis: x = A . (A <- x)
A . (A <- x) in {x} by A4, A7, FUNCT_1:def 7;
hence x = A . (A <- x) by TARSKI:def 1; :: thesis: verum