let X be set ; :: thesis:
let A, B, C be Subset of X; :: thesis:
defpred S₁[ Element of NAT , set ] means ( ( $1 = 0 implies $2 = A ) & ( $1 = 1 implies $2 = B ) & ( 1 < $1 implies $2 = C ) );
defpred S₂[ set ] means ex n being Element of NAT ex X being set st
( $1 = [n,X] & S₁[n,X] );
ex GRAF being set st
for x being set holds
( x in GRAF iff ( x in [:NAT,(bool X):] & S₂[x] ) ) from XBOOLE_0:sch 1();
then consider GRAF being set such that
A1: for x being set holds
( x in GRAF iff ( x in [:NAT,(bool X):] & S₂[x] ) ) ;
A2: GRAF is Function-like

proof

let x, y1, y2 be set ; :: according to FUNCT_1:def 1 :: thesis:
assume that
A3: [x,y1] in GRAF and
A4: [x,y2] in GRAF ; :: thesis:
A5: S₂[[x,y1]] by A1, A3;
A6: [x,y2] in [:NAT,(bool X):] by A1, A4;
A7: S₂[[x,y2]] by A1, A4;
reconsider x = x as Element of NAT by A6, ZFMISC_1:106;

per cases by NAT_1:26;

suppose A8: x = 0 ; :: thesis:

then y1 = A by A5, ZFMISC_1:33;
hence y1 = y2 by A7, A8, ZFMISC_1:33; :: thesis:

end;

suppose A9: x = 1 ; :: thesis:

then y1 = B by A5, ZFMISC_1:33;
hence y1 = y2 by A7, A9, ZFMISC_1:33; :: thesis:

end;

suppose A10: x > 1 ; :: thesis:

then y1 = C by A5, ZFMISC_1:33;
hence y1 = y2 by A7, A10, ZFMISC_1:33; :: thesis:

end;

end;

end;

A11: for x being set holds
( x in GRAF iff ( x = [0,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) ) )

proof

let x be set ; :: thesis:
A12: ( ( x = [0,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) ) implies x in GRAF )

proof

A13: ( ex n being Element of NAT st
( x = [n,C] & 1 < n ) implies x in GRAF )

proof

given n being Element of NAT such that A14: x = [n,C] and
A15: 1 < n ; :: thesis:
( S₁[n,C] & x in [:NAT,(bool X):] ) by A14, A15, ZFMISC_1:106;
hence x in GRAF by A1, A14; :: thesis:

end;

A16: ( x = [1,B] implies x in GRAF )

proof

assume A17: x = [1,B] ; :: thesis:
then x in [:NAT,(bool X):] by ZFMISC_1:106;
hence x in GRAF by A1, A17; :: thesis:

end;

A18: ( x = [0,A] implies x in GRAF )

proof

assume A19: x = [0,A] ; :: thesis:
then x in [:NAT,(bool X):] by ZFMISC_1:106;
hence x in GRAF by A1, A19; :: thesis:

end;

assume ( x = [0,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) ) ; :: thesis:
hence x in GRAF by A18, A16, A13; :: thesis:

end;

( not x in GRAF or x = [0,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) )

proof

assume x in GRAF ; :: thesis:
then ex n being Element of NAT ex X0 being set st
( x = [n,X0] & S₁[n,X0] ) by A1;
hence ( x = [0,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) ) by NAT_1:26; :: thesis:

end;

hence ( x in GRAF iff ( x = [0,A] or x = [1,B] or ex n being Element of NAT st
( x = [n,C] & 1 < n ) ) ) by A12; :: thesis:

end;

GRAF is Relation-like

proof

let p be set ; :: according to RELAT_1:def 1 :: thesis:
assume p in GRAF ; :: thesis:
then ( p = [0,A] or p = [1,B] or ex n being Element of NAT st
( p = [n,C] & 1 < n ) ) by A11;
hence ex b₁, b₂ being set st p = [b₁,b₂] ; :: thesis:

end;

then reconsider F = GRAF as Function by A2;
A20: for x being set holds
( x in NAT iff ex y being set st [x,y] in F )

proof

let x be set ; :: thesis:
thus ( x in NAT implies ex y being set st [x,y] in F ) :: thesis:

proof

assume x in NAT ; :: thesis:
then reconsider x = x as Element of NAT ;
A21: ( x = 1 implies ex y being set st [x,y] in F )

proof

assume A22: x = 1 ; :: thesis:
take B ; :: thesis:
thus [x,B] in F by A11, A22; :: thesis:

end;

A23: ( 1 < x implies ex y being set st [x,y] in F )

proof

assume A24: 1 < x ; :: thesis:
take C ; :: thesis:
thus [x,C] in F by A11, A24; :: thesis:

end;

( x = 0 implies ex y being set st [x,y] in F )

proof

assume A25: x = 0 ; :: thesis:
take A ; :: thesis:
thus [x,A] in F by A11, A25; :: thesis:

end;

hence ex y being set st [x,y] in F by A21, A23, NAT_1:26; :: thesis:

end;

given y being set such that A26: [x,y] in F ; :: thesis:
[x,y] in [:NAT,(bool X):] by A1, A26;
hence x in NAT by ZFMISC_1:106; :: thesis:

end;

then A27: dom F = NAT by RELAT_1:def 4;
A28: for y being set holds
( y in {A,B,C} iff ex x being set st
( x in dom F & y = F . x ) )

proof

let y be set ; :: thesis:
thus ( y in {A,B,C} implies ex x being set st
( x in dom F & y = F . x ) ) :: thesis:

proof

assume A29: y in {A,B,C} ; :: thesis:

per cases by A29, ENUMSET1:def 1;

suppose A30: y = A ; :: thesis:

take 0 ; :: thesis:
[0,y] in F by A11, A30;
hence ( 0 in dom F & y = F . 0 ) by FUNCT_1:8; :: thesis:

end;

suppose A31: y = B ; :: thesis:

take 1 ; :: thesis:
[1,y] in F by A11, A31;
hence ( 1 in dom F & y = F . 1 ) by FUNCT_1:8; :: thesis:

end;

suppose A32: y = C ; :: thesis:

take 2 ; :: thesis:
[2,y] in F by A11, A32;
hence ( 2 in dom F & y = F . 2 ) by FUNCT_1:8; :: thesis:

end;

end;

end;

given x being set such that A33: x in dom F and
A34: y = F . x ; :: thesis:
reconsider x = x as Element of NAT by A20, A33, RELAT_1:def 4;

per cases by NAT_1:26;

suppose A35: x = 0 ; :: thesis:

[0,A] in F by A11;
then A = F . x by A35, FUNCT_1:8;
hence y in {A,B,C} by A34, ENUMSET1:def 1; :: thesis:

end;

suppose A36: x = 1 ; :: thesis:

[1,B] in F by A11;
then B = F . x by A36, FUNCT_1:8;
hence y in {A,B,C} by A34, ENUMSET1:def 1; :: thesis:

end;

suppose 1 < x ; :: thesis:

then [x,C] in F by A11;
then y = C by A34, FUNCT_1:8;
hence y in {A,B,C} by ENUMSET1:def 1; :: thesis:

end;

end;

end;

then A37: rng F = {A,B,C} by FUNCT_1:def 5;
rng F c= bool X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in rng F ; :: thesis:
then ( a = A or a = B or a = C ) by A37, ENUMSET1:def 1;
hence a in bool X ; :: thesis:

end;

then reconsider F = F as Function of NAT,(bool X) by A27, FUNCT_2:4;
A38: for n being Element of NAT st 1 < n holds
F . n = C

proof

let n be Element of NAT ; :: thesis:
assume 1 < n ; :: thesis:
then [n,C] in F by A11;
hence F . n = C by FUNCT_1:8; :: thesis:

end;

take F ; :: thesis:
( [0,A] in F & [1,B] in F ) by A11;
hence ( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) ) by A28, A38, FUNCT_1:8, FUNCT_1:def 5; :: thesis: