defpred S₁[ set ] means ex G being Function of (Fin X),Y st
( ( for e being Element of Y st e is_a_unity_wrt F holds
G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= $1 & B9 <> {} holds
for x being Element of X st x in $1 \ B9 holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) );
A4: for B9 being Element of Fin X
for b being Element of X st S₁[B9] & not b in B9 holds
S₁[B9 \/ {b}]

let B be Element of Fin X; :: thesis:
let x be Element of X; :: thesis:
given G being Function of (Fin X),Y such that A5: for e being Element of Y st e is_a_unity_wrt F holds
G . {} = e and
A6: for x being Element of X holds G . {x} = f . x and
A7: for B9 being Element of Fin X st B9 c= B & B9 <> {} holds
for x being Element of X st x in B \ B9 holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ; :: thesis:
assume A8: not x in B ; :: thesis:
thus ex G being Function of (Fin X),Y st
( ( for e being Element of Y st e is_a_unity_wrt F holds
G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B \/ {x} & B9 <> {} holds
for x9 being Element of X st x9 in (B \/ {x}) \ B9 holds
G . (B9 \/ {x9}) = F . ((G . B9),(f . x9)) ) ) :: thesis:

defpred S₂[ set , set ] means ( ( for C being Element of Fin X st C <> {} & C c= B & $1 = C \/ {.x.} holds
$2 = F . ((G . C),(f . x)) ) & ( ( for C being Element of Fin X holds
( not C <> {} or not C c= B or not $1 = C \/ {.x.} ) ) implies $2 = G . $1 ) );

A9: now :: thesis:

let B9 be Element of Fin X; :: thesis:
thus ex y being Element of Y st S₂[B9,y] :: thesis:

proof

A10: now :: thesis:

given C being Element of Fin X such that A11: C <> {} and
A12: C c= B and
A13: B9 = C \/ {x} ; :: thesis:
take y = F . ((G . C),(f . x)); :: thesis:
for C being Element of Fin X st C <> {} & C c= B & B9 = C \/ {x} holds
y = F . ((G . C),(f . x))

proof

not x in C by A8, A12;
then A14: C c= B9 \ {x} by A13, XBOOLE_1:7, ZFMISC_1:34;
B9 \ {x} = C \ {x} by A13, XBOOLE_1:40;
then A15: B9 \ {x} = C by A14, XBOOLE_0:def 10;
let C1 be Element of Fin X; :: thesis:
assume that
C1 <> {} and
A16: C1 c= B and
A17: B9 = C1 \/ {x} ; :: thesis:
not x in C1 by A8, A16;
then A18: C1 c= B9 \ {x} by A17, XBOOLE_1:7, ZFMISC_1:34;
B9 \ {x} = C1 \ {x} by A17, XBOOLE_1:40;
hence y = F . ((G . C1),(f . x)) by A18, A15, XBOOLE_0:def 10; :: thesis:

end;

hence ex y being Element of Y st S₂[B9,y] by A11, A12, A13; :: thesis:

end;

now :: thesis:

assume A19: for C being Element of Fin X holds
( not C <> {} or not C c= B or not B9 = C \/ {x} ) ; :: thesis:
take y = G . B9; :: thesis:
thus for C being Element of Fin X st C <> {} & C c= B & B9 = C \/ {x} holds
y = F . ((G . C),(f . x)) by A19; :: thesis:
thus ( ( for C being Element of Fin X holds
( not C <> {} or not C c= B or not B9 = C \/ {x} ) ) implies y = G . B9 ) ; :: thesis:

end;

hence ex y being Element of Y st S₂[B9,y] by A10; :: thesis:

end;

consider H being Function of (Fin X),Y such that
A20: for B9 being Element of Fin X holds S₂[B9,H . B9] from FUNCT_2:sch 3(A9);
take J = H; :: thesis:

now :: thesis:

given C being Element of Fin X such that A21: C <> {} and
A22: C c= B and
A23: {x} = C \/ {x} ; :: thesis:
C = {x} by A21, A23, XBOOLE_1:7, ZFMISC_1:33;
then x in C by TARSKI:def 1;
hence contradiction by A8, A22; :: thesis:

end;

then A24: J . {x} = G . {.x.} by A20;
thus for e being Element of Y st e is_a_unity_wrt F holds
J . {} = e :: thesis:

proof

reconsider E = {} as Element of Fin X by FINSUB_1:7;
for C being Element of Fin X holds
( not C <> {} or not C c= B or not E = C \/ {x} ) ;
then J . E = G . E by A20;
hence for e being Element of Y st e is_a_unity_wrt F holds
J . {} = e by A5; :: thesis:

end;

thus for x being Element of X holds J . {x} = f . x :: thesis:

proof

let x9 be Element of X; :: thesis:

now :: thesis:

given C being Element of Fin X such that A25: C <> {} and
A26: C c= B and
A27: {x9} = C \/ {x} ; :: thesis:
A28: C = {x9} by A25, A27, XBOOLE_1:7, ZFMISC_1:33;
x = x9 by A27, XBOOLE_1:7, ZFMISC_1:18;
then x in C by A28, TARSKI:def 1;
hence contradiction by A8, A26; :: thesis:

end;

hence J . {x9} = G . {.x9.} by A20
.= f . x9 by A6 ;
:: thesis:

end;

let B9 be Element of Fin X; :: thesis:
assume that
A29: B9 c= B \/ {x} and
A30: B9 <> {} ; :: thesis:
let x9 be Element of X; :: thesis:
assume A31: x9 in (B \/ {x}) \ B9 ; :: thesis:
then A32: not x9 in B9 by XBOOLE_0:def 5;

per cases ;

suppose A33: x in B9 ; :: thesis:

then A34: x9 in B by A31, A32, ZFMISC_1:136;

per cases ;

suppose A35: B9 = {x} ; :: thesis:

hence J . (B9 \/ {.x9.}) = F . ((G . {.x9.}),(f . x)) by A20, A34, ZFMISC_1:31
.= F . ((f . x9),(f . x)) by A6
.= F . ((f . x),(f . x9)) by A2
.= F . ((J . B9),(f . x9)) by A6, A24, A35 ;
:: thesis:

end;

suppose B9 <> {x} ; :: thesis:

then not B9 c= {x} by A30, ZFMISC_1:33;
then A36: B9 \ {x} <> {} by XBOOLE_1:37;
set C = (B9 \ {.x.}) \/ {.x9.};
not x9 in B9 \ {x} by A31, XBOOLE_0:def 5;
then A37: x9 in B \ (B9 \ {x}) by A34, XBOOLE_0:def 5;
B9 \ {x} c= B by A29, XBOOLE_1:43;
then A38: (B9 \ {.x.}) \/ {.x9.} c= B by A33, A31, A32, ZFMISC_1:136, ZFMISC_1:137;
B9 \/ {.x9.} = (B9 \/ {x}) \/ {x9} by A33, ZFMISC_1:40
.= ((B9 \ {x}) \/ {x}) \/ {x9} by XBOOLE_1:39
.= ((B9 \ {.x.}) \/ {.x9.}) \/ {.x.} by XBOOLE_1:4 ;
hence J . (B9 \/ {.x9.}) = F . ((G . ((B9 \ {.x.}) \/ {.x9.})),(f . x)) by A20, A38
.= F . ((F . ((G . (B9 \ {.x.})),(f . x9))),(f . x)) by A7, A29, A36, A37, XBOOLE_1:43
.= F . ((G . (B9 \ {.x.})),(F . ((f . x9),(f . x)))) by A3
.= F . ((G . (B9 \ {x})),(F . ((f . x),(f . x9)))) by A2
.= F . ((F . ((G . (B9 \ {.x.})),(f . x))),(f . x9)) by A3
.= F . ((J . ((B9 \ {.x.}) \/ {.x.})),(f . x9)) by A20, A29, A36, XBOOLE_1:43
.= F . ((J . (B9 \/ {x})),(f . x9)) by XBOOLE_1:39
.= F . ((J . B9),(f . x9)) by A33, ZFMISC_1:40 ;
:: thesis:

end;

suppose A39: not x in B9 ; :: thesis:

then A40: B9 c= B by A29, ZFMISC_1:135;
A41: for C being Element of Fin X holds
( not C <> {} or not C c= B or not B9 = C \/ {x} ) by A39, ZFMISC_1:136;

per cases ;

suppose A42: x <> x9 ; :: thesis:

then x9 in B by A31, ZFMISC_1:136;
then A43: x9 in B \ B9 by A32, XBOOLE_0:def 5;
not x in B9 \/ {x9} by A39, A42, ZFMISC_1:136;
then for C being Element of Fin X holds
( not C <> {} or not C c= B or not B9 \/ {x9} = C \/ {x} ) by ZFMISC_1:136;
hence J . (B9 \/ {.x9.}) = G . (B9 \/ {.x9.}) by A20
.= F . ((G . B9),(f . x9)) by A7, A30, A40, A43
.= F . ((J . B9),(f . x9)) by A20, A41 ;
:: thesis:

end;

suppose x = x9 ; :: thesis:

hence J . (B9 \/ {.x9.}) = F . ((G . B9),(f . x9)) by A20, A29, A30, A39, ZFMISC_1:135
.= F . ((J . B9),(f . x9)) by A20, A41 ;
:: thesis:

end;

A44: S₁[ {}. X]

proof

consider e being Element of Y such that
A45: ( ex e being Element of Y st e is_a_unity_wrt F implies e = the_unity_wrt F ) ;
defpred S₂[ set , set ] means ( ( for x9 being Element of X st $1 = {x9} holds
$2 = f . x9 ) & ( ( for x9 being Element of X holds not $1 = {x9} ) implies $2 = e ) );

A46: now :: thesis:

let x be Element of Fin X; :: thesis:

A47: now :: thesis:

given x9 being Element of X such that A48: x = {x9} ; :: thesis:
take y = f . x9; :: thesis:
thus for x9 being Element of X st x = {x9} holds
y = f . x9 by A48, ZFMISC_1:3; :: thesis:
thus ( ( for x9 being Element of X holds not x = {x9} ) implies y = e ) by A48; :: thesis:

end;

now :: thesis:

assume A49: for x9 being Element of X holds not x = {x9} ; :: thesis:
take y = e; :: thesis:
thus ( ( for x9 being Element of X st x = {x9} holds
y = f . x9 ) & ( ( for x9 being Element of X holds not x = {x9} ) implies y = e ) ) by A49; :: thesis:

end;

hence ex y being Element of Y st S₂[x,y] by A47; :: thesis:

end;

consider G9 being Function of (Fin X),Y such that
A50: for B9 being Element of Fin X holds S₂[B9,G9 . B9] from FUNCT_2:sch 3(A46);
take G = G9; :: thesis:
thus for e being Element of Y st e is_a_unity_wrt F holds
G . {} = e :: thesis:

proof

reconsider E = {} as Element of Fin X by FINSUB_1:7;
let e9 be Element of Y; :: thesis:
assume A51: e9 is_a_unity_wrt F ; :: thesis:
for x9 being Element of X holds not E = {x9} ;
hence G . {} = e by A50
.= e9 by A45, A51, BINOP_1:def 8 ;
:: thesis:

end;

thus for x being Element of X holds G . {.x.} = f . x by A50; :: thesis:
thus for B9 being Element of Fin X st B9 c= {}. X & B9 <> {} holds
for x being Element of X st x in ({}. X) \ B9 holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ; :: thesis:

end;

for B being Element of Fin X holds S₁[B] from SETWISEO:sch 2(A44, A4);
then consider G being Function of (Fin X),Y such that
A52: ( ( for e being Element of Y st e is_a_unity_wrt F holds
G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B & B9 <> {} holds
for x being Element of X st x in B \ B9 holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ;
take G . B ; :: thesis:
take G ; :: thesis:
thus ( G . B = G . B & ( for e being Element of Y st e is_a_unity_wrt F holds
G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B & B9 <> {} holds
for x being Element of X st x in B \ B9 holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) by A52; :: thesis: