defpred S1[ 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 S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
proof
let B be Element of Fin X; :: thesis: for b being Element of X st S1[B] & not b in B holds
S1[B \/ {b}]
let x be Element of X; :: thesis: ( S1[B] & not x in B implies S1[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 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: ( x in B or S1[B \/ {x}] )
assume A8: not x in B ; :: thesis: S1[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 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: verum
proof
defpred S2[ 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: for B9 being Element of Fin X ex y being Element of Y st S2[B9,y]
let B9 be Element of Fin X; :: thesis: ex y being Element of Y st S2[B9,y]
thus ex y being Element of Y st S2[B9,y] :: thesis: verum
proof
A10: now :: thesis: ( ex C being Element of Fin X st
( C <> {} & C c= B & B9 = C \/ {x} ) implies ex y being Element of Y ex y being Element of Y st S2[B9,y] )
given C being Element of Fin X such that A11: C <> {} and
A12: C c= B and
A13: B9 = C \/ {x} ; :: thesis: ex y being Element of Y ex y being Element of Y st S2[B9,y]
take y = F . ((G . C),(f . x)); :: thesis: ex y being Element of Y st S2[B9,y]
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: ( C1 <> {} & C1 c= B & B9 = C1 \/ {x} implies y = F . ((G . C1),(f . x)) )
assume that
C1 <> {} and
A16: C1 c= B and
A17: B9 = C1 \/ {x} ; :: thesis: y = F . ((G . C1),(f . x))
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: verum
end;
hence ex y being Element of Y st S2[B9,y] by A11, A12, A13; :: thesis: verum
end;
now :: thesis: ( ( for C being Element of Fin X holds
( not C <> {} or not C c= B or not B9 = C \/ {x} ) ) implies ex y being Element of Y st
( ( for C being Element of Fin X st C <> {} & C c= B & B9 = 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 B9 = C \/ {x} ) ) implies y = G . B9 ) ) )
assume A19: for C being Element of Fin X holds
( not C <> {} or not C c= B or not B9 = C \/ {x} ) ; :: thesis: ex y being Element of Y st
( ( for C being Element of Fin X st C <> {} & C c= B & B9 = 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 B9 = C \/ {x} ) ) implies y = G . B9 ) )
take y = G . B9; :: thesis: ( ( for C being Element of Fin X st C <> {} & C c= B & B9 = 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 B9 = C \/ {x} ) ) implies y = G . B9 ) )
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: ( ( for C being Element of Fin X holds
( not C <> {} or not C c= B or not B9 = C \/ {x} ) ) implies y = G . B9 )
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: verum
end;
hence ex y being Element of Y st S2[B9,y] by A10; :: thesis: verum
end;
end;
consider H being Function of (Fin X),Y such that
A20: for B9 being Element of Fin X holds S2[B9,H . B9] 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 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
J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) ) )
now :: thesis: for C being Element of Fin X holds
( not C <> {} or not C c= B or not {x} = C \/ {x} )
given C being Element of Fin X such that A21: C <> {} and
A22: C c= B and
A23: {x} = C \/ {x} ; :: thesis: contradiction
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: 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 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
J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) ) )
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: verum
end;
thus for x being Element of X holds J . {x} = f . x :: thesis: 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
J . (B9 \/ {x9}) = F . ((J . B9),(f . x9))
proof
let x9 be Element of X; :: thesis: J . {x9} = f . x9
now :: thesis: for C being Element of Fin X holds
( not C <> {} or not C c= B or not {x9} = C \/ {x} )
given C being Element of Fin X such that A25: C <> {} and
A26: C c= B and
A27: {x9} = C \/ {x} ; :: thesis: contradiction
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: verum
end;
hence J . {x9} = G . {.x9.} by A20
.= f . x9 by A6 ;
:: thesis: verum
end;
let B9 be Element of Fin X; :: thesis: ( B9 c= B \/ {x} & B9 <> {} implies for x9 being Element of X st x9 in (B \/ {x}) \ B9 holds
J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) )
assume that
A29: B9 c= B \/ {x} and
A30: B9 <> {} ; :: thesis: for x9 being Element of X st x9 in (B \/ {x}) \ B9 holds
J . (B9 \/ {x9}) = F . ((J . B9),(f . x9))
let x9 be Element of X; :: thesis: ( x9 in (B \/ {x}) \ B9 implies J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) )
assume A31: x9 in (B \/ {x}) \ B9 ; :: thesis: J . (B9 \/ {x9}) = F . ((J . B9),(f . x9))
then A32: not x9 in B9 by XBOOLE_0:def 5;
per cases ( x in B9 or not x in B9 ) ;
suppose A33: x in B9 ; :: thesis: J . (B9 \/ {x9}) = F . ((J . B9),(f . x9))
then A34: x9 in B by A31, A32, ZFMISC_1:136;
per cases ( B9 = {x} or B9 <> {x} ) ;
suppose A35: B9 = {x} ; :: thesis: J . (B9 \/ {x9}) = F . ((J . B9),(f . x9))
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: verum
end;
suppose B9 <> {x} ; :: thesis: J . (B9 \/ {x9}) = F . ((J . B9),(f . x9))
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: verum
end;
end;
end;
suppose A39: not x in B9 ; :: thesis: J . (B9 \/ {x9}) = F . ((J . B9),(f . x9))
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 ( x <> x9 or x = x9 ) ;
suppose A42: x <> x9 ; :: thesis: J . (B9 \/ {x9}) = F . ((J . B9),(f . x9))
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: verum
end;
suppose x = x9 ; :: thesis: J . (B9 \/ {x9}) = F . ((J . B9),(f . x9))
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: verum
end;
end;
end;
end;
end;
end;
A44: S1[ {}. 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 S2[ 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: for x being Element of Fin X ex y being Element of Y st S2[x,y]
let x be Element of Fin X; :: thesis: ex y being Element of Y st S2[x,y]
A47: now :: thesis: ( ex x9 being Element of X st x = {x9} implies ex y being Element of Y st
( ( 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 ) ) )
given x9 being Element of X such that A48: x = {x9} ; :: thesis: ex y being Element of Y st
( ( 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 ) )
take y = f . x9; :: thesis: ( ( 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 ) )
thus for x9 being Element of X st x = {x9} holds
y = f . x9 by A48, ZFMISC_1:3; :: thesis: ( ( for x9 being Element of X holds not x = {x9} ) implies y = e )
thus ( ( for x9 being Element of X holds not x = {x9} ) implies y = e ) by A48; :: thesis: verum
end;
now :: thesis: ( ( for x9 being Element of X holds not x = {x9} ) implies ex y being Element of Y st
( ( 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 ) ) )
assume A49: for x9 being Element of X holds not x = {x9} ; :: thesis: ex y being Element of Y st
( ( 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 ) )
take y = e; :: thesis: ( ( 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 ) )
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: verum
end;
hence ex y being Element of Y st S2[x,y] by A47; :: thesis: verum
end;
consider G9 being Function of (Fin X),Y such that
A50: for B9 being Element of Fin X holds S2[B9,G9 . B9] from FUNCT_2:sch 3(A46);
 take G = G9; :: 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 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)) ) )
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 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)) ) )
proof
reconsider E = {} as Element of Fin X by FINSUB_1:7;
let e9 be Element of Y; :: thesis: ( e9 is_a_unity_wrt F implies G . {} = e9 )
assume A51: e9 is_a_unity_wrt F ; :: thesis: G . {} = e9
for x9 being Element of X holds not E = {x9} ;
hence G . {} = e by A50
.= e9 by A45, A51, BINOP_1:def 8 ;
:: thesis: verum
end;
thus for x being Element of X holds G . {.x.} = f . x by A50; :: thesis: 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))
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: verum
end;
for B being Element of Fin X holds S1[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: 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 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 ; :: 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 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)) ) )
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: verum