let x, y be Element of Y; :: thesis: ( ex G being Function of (Fin X),Y st
( x = 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)) ) ) & ex G being Function of (Fin X),Y st
( y = 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)) ) ) implies x = y )
given G1 being Function of (Fin X),Y such that A53: x = G1 . B and
A54: for e being Element of Y st e is_a_unity_wrt F holds
G1 . {} = e and
A55: for x being Element of X holds G1 . {x} = f . x and
A56: 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
G1 . (B9 \/ {x}) = F . ((G1 . B9),(f . x)) ; :: thesis: ( for G being Function of (Fin X),Y holds
( not y = G . B or ex e being Element of Y st
( e is_a_unity_wrt F & not G . {} = e ) or ex x being Element of X st not G . {x} = f . x or ex B9 being Element of Fin X st
( B9 c= B & B9 <> {} & ex x being Element of X st
( x in B \ B9 & not G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ) or x = y )
given G2 being Function of (Fin X),Y such that A57: y = G2 . B and
A58: for e being Element of Y st e is_a_unity_wrt F holds
G2 . {} = e and
A59: for x being Element of X holds G2 . {x} = f . x and
A60: 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
G2 . (B9 \/ {x}) = F . ((G2 . B9),(f . x)) ; :: thesis: x = y
per cases ( B = {} or B <> {} ) ;
suppose A61: B = {} ; :: thesis: x = y
thus x = the_unity_wrt F by A53, A54, A61, A1, Th11
.= y by A57, A58, A61, A1, Th11 ; :: thesis: verum
end;
suppose A62: B <> {} ; :: thesis: x = y
defpred S1[ set ] means ( $1 c= B & $1 <> {} implies G1 . $1 = G2 . $1 );
A63: 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 B9 be Element of Fin X; :: thesis: for b being Element of X st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
let x be Element of X; :: thesis: ( S1[B9] & not x in B9 implies S1[B9 \/ {x}] )
assume A64: ( B9 c= B & B9 <> {} implies G1 . B9 = G2 . B9 ) ; :: thesis: ( x in B9 or S1[B9 \/ {x}] )
assume A65: not x in B9 ; :: thesis: S1[B9 \/ {x}]
assume A66: B9 \/ {x} c= B ; :: thesis: ( not B9 \/ {x} <> {} or G1 . (B9 \/ {x}) = G2 . (B9 \/ {x}) )
then A67: B9 c= B by ZFMISC_1:137;
assume B9 \/ {x} <> {} ; :: thesis: G1 . (B9 \/ {x}) = G2 . (B9 \/ {x})
x in B by A66, ZFMISC_1:137;
then A68: x in B \ B9 by A65, XBOOLE_0:def 5;
per cases ( B9 = {} or B9 <> {} ) ;
suppose A69: B9 = {} ; :: thesis: G1 . (B9 \/ {x}) = G2 . (B9 \/ {x})
hence G1 . (B9 \/ {x}) = f . x by A55
.= G2 . (B9 \/ {x}) by A59, A69 ;
:: thesis: verum
end;
suppose A70: B9 <> {} ; :: thesis: G1 . (B9 \/ {x}) = G2 . (B9 \/ {x})
hence G1 . (B9 \/ {x}) = F . ((G1 . B9),(f . x)) by A56, A67, A68
.= G2 . (B9 \/ {x}) by A60, A64, A67, A68, A70 ;
:: thesis: verum
end;
end;
end;
A71: S1[ {}. X] ;
for B9 being Element of Fin X holds S1[B9] from SETWISEO:sch 2(A71, A63);
hence x = y by A53, A57, A62; :: thesis: verum
end;
end;