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 B' being Element of Fin X st B' c= $1 & B' <> {} holds
for x being Element of X st x in $1 \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) );
A4: for B' being Element of Fin X
for b being Element of X st S₁[B'] & not b in B' holds
S₁[B' \/ {b}]

proof

let B be Element of Fin X; :: thesis: for b being Element of X st S₁[B] & not b in B holds
S₁[B \/ {b}]
let x be Element of X; :: thesis: ( S₁[B] & not x in B implies S₁[B \/ {x}] )
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 B' being Element of Fin X st B' c= B & B' <> {} holds
for x being Element of X st x in B \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ; :: thesis: ( x in B or S₁[B \/ {x}] )
assume A8: not x in B ; :: thesis: S₁[B \/ {x}]
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 B' being Element of Fin X st B' c= B \/ {x} & B' <> {} holds
for x' being Element of X st x' in (B \/ {x}) \ B' holds
G . (B' \/ {x'}) = F . (G . B'),(f . x') ) ) :: thesis: verum

proof

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

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

proof

A10: now

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

proof

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

end;

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

end;

now

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

end;

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

end;

end;

consider H being Function of Fin X,Y such that
A20: for B' being Element of Fin X holds S₂[B',H . B'] from FUNCT_2:sch 3(A9);
take J = H; :: thesis: ( ( for e being Element of Y st e is_a_unity_wrt F holds
J . {} = e ) & ( for x being Element of X holds J . {x} = f . x ) & ( for B' being Element of Fin X st B' c= B \/ {x} & B' <> {} holds
for x' being Element of X st x' in (B \/ {x}) \ B' holds
J . (B' \/ {x'}) = F . (J . B'),(f . x') ) )

now

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

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: ( ( for x being Element of X holds J . {x} = f . x ) & ( for B' being Element of Fin X st B' c= B \/ {x} & B' <> {} holds
for x' being Element of X st x' in (B \/ {x}) \ B' holds
J . (B' \/ {x'}) = F . (J . B'),(f . x') ) )

proof

reconsider E = {} as Element of Fin X by FINSUB_1:18;
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: verum

end;

thus for x being Element of X holds J . {x} = f . x :: thesis: for B' being Element of Fin X st B' c= B \/ {x} & B' <> {} holds
for x' being Element of X st x' in (B \/ {x}) \ B' holds
J . (B' \/ {x'}) = F . (J . B'),(f . x')

proof

let x' be Element of X; :: thesis: J . {x'} = f . x'

now

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

end;

hence J . {x'} = G . {.x'.} by A20
.= f . x' by A6 ;
:: thesis: verum

end;

let B' be Element of Fin X; :: thesis: ( B' c= B \/ {x} & B' <> {} implies for x' being Element of X st x' in (B \/ {x}) \ B' holds
J . (B' \/ {x'}) = F . (J . B'),(f . x') )
assume that
A29: B' c= B \/ {x} and
A30: B' <> {} ; :: thesis: for x' being Element of X st x' in (B \/ {x}) \ B' holds
J . (B' \/ {x'}) = F . (J . B'),(f . x')
let x' be Element of X; :: thesis: ( x' in (B \/ {x}) \ B' implies J . (B' \/ {x'}) = F . (J . B'),(f . x') )
assume A31: x' in (B \/ {x}) \ B' ; :: thesis: J . (B' \/ {x'}) = F . (J . B'),(f . x')
then A32: not x' in B' by XBOOLE_0:def 5;

per cases ( x in B' or not x in B' ) ;

suppose A33: x in B' ; :: thesis: J . (B' \/ {x'}) = F . (J . B'),(f . x')

then A34: x' in B by A31, A32, Th6;
then A35: {x'} c= B by ZFMISC_1:37;

per cases ( B' = {x} or B' <> {x} ) ;

suppose A36: B' = {x} ; :: thesis: J . (B' \/ {x'}) = F . (J . B'),(f . x')

hence J . (B' \/ {.x'.}) = F . (G . {.x'.}),(f . x) by A20, A35
.= F . (f . x'),(f . x) by A6
.= F . (f . x),(f . x') by A2, BINOP_1:def 2
.= F . (J . B'),(f . x') by A6, A24, A36 ;
:: thesis: verum

end;

suppose B' <> {x} ; :: thesis: J . (B' \/ {x'}) = F . (J . B'),(f . x')

then not B' c= {x} by A30, ZFMISC_1:39;
then A37: B' \ {x} <> {} by XBOOLE_1:37;
set C = (B' \ {.x.}) \/ {.x'.};
not x' in B' \ {x} by A31, XBOOLE_0:def 5;
then A38: x' in B \ (B' \ {x}) by A34, XBOOLE_0:def 5;
B' \ {x} c= B by A29, XBOOLE_1:43;
then A39: (B' \ {.x.}) \/ {.x'.} c= B by A34, Th8;
B' \/ {.x'.} = (B' \/ {x}) \/ {x'} by A33, ZFMISC_1:46
.= ((B' \ {x}) \/ {x}) \/ {x'} by XBOOLE_1:39
.= ((B' \ {.x.}) \/ {.x'.}) \/ {.x.} by XBOOLE_1:4 ;
hence J . (B' \/ {.x'.}) = F . (G . ((B' \ {.x.}) \/ {.x'.})),(f . x) by A20, A39
.= F . (F . (G . (B' \ {.x.})),(f . x')),(f . x) by A7, A29, A37, A38, XBOOLE_1:43
.= F . (G . (B' \ {.x.})),(F . (f . x'),(f . x)) by A3, BINOP_1:def 3
.= F . (G . (B' \ {x})),(F . (f . x),(f . x')) by A2, BINOP_1:def 2
.= F . (F . (G . (B' \ {.x.})),(f . x)),(f . x') by A3, BINOP_1:def 3
.= F . (J . ((B' \ {.x.}) \/ {.x.})),(f . x') by A20, A29, A37, XBOOLE_1:43
.= F . (J . (B' \/ {x})),(f . x') by XBOOLE_1:39
.= F . (J . B'),(f . x') by A33, ZFMISC_1:46 ;
:: thesis: verum

end;

end;

end;

suppose A40: not x in B' ; :: thesis: J . (B' \/ {x'}) = F . (J . B'),(f . x')

then A41: B' c= B by A29, Th5;
A42: for C being Element of Fin X holds
( not C <> {} or not C c= B or not B' = C \/ {x} ) by A40, Th6;

per cases ( x <> x' or x = x' ) ;

suppose A43: x <> x' ; :: thesis: J . (B' \/ {x'}) = F . (J . B'),(f . x')

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

end;

suppose x = x' ; :: thesis: J . (B' \/ {x'}) = F . (J . B'),(f . x')

hence J . (B' \/ {.x'.}) = F . (G . B'),(f . x') by A20, A29, A30, A40, Th5
.= F . (J . B'),(f . x') by A20, A42 ;
:: thesis: verum

end;

end;

end;

end;

end;

end;

A45: S₁[ {}. X]

proof

consider e being Element of Y such that
A46: ( 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 x' being Element of X st $1 = {x'} holds
$2 = f . x' ) & ( ( for x' being Element of X holds not $1 = {x'} ) implies $2 = e ) );

A47: now

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

A48: now

given x' being Element of X such that A49: x = {x'} ; :: thesis: ex y being Element of Y st
( ( for x' being Element of X st x = {x'} holds
y = f . x' ) & ( ( for x' being Element of X holds not x = {x'} ) implies y = e ) )
take y = f . x'; :: thesis: ( ( for x' being Element of X st x = {x'} holds
y = f . x' ) & ( ( for x' being Element of X holds not x = {x'} ) implies y = e ) )
thus for x' being Element of X st x = {x'} holds
y = f . x' by A49, ZFMISC_1:6; :: thesis: ( ( for x' being Element of X holds not x = {x'} ) implies y = e )
thus ( ( for x' being Element of X holds not x = {x'} ) implies y = e ) by A49; :: thesis: verum

end;

now

assume A50: for x' being Element of X holds not x = {x'} ; :: thesis: ex y being Element of Y st
( ( for x' being Element of X st x = {x'} holds
y = f . x' ) & ( ( for x' being Element of X holds not x = {x'} ) implies y = e ) )
take y = e; :: thesis: ( ( for x' being Element of X st x = {x'} holds
y = f . x' ) & ( ( for x' being Element of X holds not x = {x'} ) implies y = e ) )
thus ( ( for x' being Element of X st x = {x'} holds
y = f . x' ) & ( ( for x' being Element of X holds not x = {x'} ) implies y = e ) ) by A50; :: thesis: verum

end;

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

end;

consider G' being Function of Fin X,Y such that
A51: for B' being Element of Fin X holds S₂[B',G' . B'] from FUNCT_2:sch 3(A47);
take G = G'; :: thesis: ( ( 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 B' being Element of Fin X st B' c= {}. X & B' <> {} holds
for x being Element of X st x in ({}. X) \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) )
thus for e being Element of Y st e is_a_unity_wrt F holds
G . {} = e :: thesis: ( ( for x being Element of X holds G . {x} = f . x ) & ( for B' being Element of Fin X st B' c= {}. X & B' <> {} holds
for x being Element of X st x in ({}. X) \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) )

proof

reconsider E = {} as Element of Fin X by FINSUB_1:18;
let e' be Element of Y; :: thesis: ( e' is_a_unity_wrt F implies G . {} = e' )
assume A52: e' is_a_unity_wrt F ; :: thesis: G . {} = e'
for x' being Element of X holds not E = {x'} ;
hence G . {} = e by A51
.= e' by A46, A52, BINOP_1:def 8 ;
:: thesis: verum

end;

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

end;

for B being Element of Fin X holds S₁[B] from SETWISEO:sch 2(A45, A4);
then consider G being Function of Fin X,Y such that
A53: ( ( 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 B' being Element of Fin X st B' c= B & B' <> {} holds
for x being Element of X st x in B \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) ) ;
take G . B ; :: thesis: ex G being Function of Fin X,Y st
( 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 B' being Element of Fin X st B' c= B & B' <> {} holds
for x being Element of X st x in B \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) )
take G ; :: thesis: ( 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 B' being Element of Fin X st B' c= B & B' <> {} holds
for x being Element of X st x in B \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) )
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 B' being Element of Fin X st B' c= B & B' <> {} holds
for x being Element of X st x in B \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) ) by A53; :: thesis: verum