let M be non empty set ; :: thesis: for H being ZF-formula
for F, G being Function st F is_definable_in M & G is_definable_in M & Free H c= {(x. 3)} holds
for FG being Function st dom FG = M & ( for v being Function of VAR,M holds
( ( M,v |= H implies FG . (v . (x. 3)) = F . (v . (x. 3)) ) & ( M,v |= 'not' H implies FG . (v . (x. 3)) = G . (v . (x. 3)) ) ) ) holds
FG is_definable_in M
let H be ZF-formula; :: thesis: for F, G being Function st F is_definable_in M & G is_definable_in M & Free H c= {(x. 3)} holds
for FG being Function st dom FG = M & ( for v being Function of VAR,M holds
( ( M,v |= H implies FG . (v . (x. 3)) = F . (v . (x. 3)) ) & ( M,v |= 'not' H implies FG . (v . (x. 3)) = G . (v . (x. 3)) ) ) ) holds
FG is_definable_in M
let F, G be Function; :: thesis: ( F is_definable_in M & G is_definable_in M & Free H c= {(x. 3)} implies for FG being Function st dom FG = M & ( for v being Function of VAR,M holds
( ( M,v |= H implies FG . (v . (x. 3)) = F . (v . (x. 3)) ) & ( M,v |= 'not' H implies FG . (v . (x. 3)) = G . (v . (x. 3)) ) ) ) holds
FG is_definable_in M )
A1: {(x. 3),(x. 3),(x. 4)} = {(x. 3),(x. 4)} by ENUMSET1:30;
A2: {(x. 3)} \/ {(x. 3),(x. 4)} = {(x. 3),(x. 3),(x. 4)} by ENUMSET1:2;
given H1 being ZF-formula such that A3: Free H1 c= {(x. 3),(x. 4)} and
A4: M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) and
A5: F = def_func (H1,M) ; :: according to ZFMODEL1:def 3 :: thesis: ( not G is_definable_in M or not Free H c= {(x. 3)} or for FG being Function st dom FG = M & ( for v being Function of VAR,M holds
( ( M,v |= H implies FG . (v . (x. 3)) = F . (v . (x. 3)) ) & ( M,v |= 'not' H implies FG . (v . (x. 3)) = G . (v . (x. 3)) ) ) ) holds
FG is_definable_in M )
given H2 being ZF-formula such that A6: Free H2 c= {(x. 3),(x. 4)} and
A7: M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) and
A8: G = def_func (H2,M) ; :: according to ZFMODEL1:def 3 :: thesis: ( not Free H c= {(x. 3)} or for FG being Function st dom FG = M & ( for v being Function of VAR,M holds
( ( M,v |= H implies FG . (v . (x. 3)) = F . (v . (x. 3)) ) & ( M,v |= 'not' H implies FG . (v . (x. 3)) = G . (v . (x. 3)) ) ) ) holds
FG is_definable_in M )
assume A9: Free H c= {(x. 3)} ; :: thesis: for FG being Function st dom FG = M & ( for v being Function of VAR,M holds
( ( M,v |= H implies FG . (v . (x. 3)) = F . (v . (x. 3)) ) & ( M,v |= 'not' H implies FG . (v . (x. 3)) = G . (v . (x. 3)) ) ) ) holds
FG is_definable_in M
then A10: not x. 4 in Free H by Lm3, TARSKI:def 1;
let FG be Function; :: thesis: ( dom FG = M & ( for v being Function of VAR,M holds
( ( M,v |= H implies FG . (v . (x. 3)) = F . (v . (x. 3)) ) & ( M,v |= 'not' H implies FG . (v . (x. 3)) = G . (v . (x. 3)) ) ) ) implies FG is_definable_in M )
assume that
A11: dom FG = M and
A12: for v being Function of VAR,M holds
( ( M,v |= H implies FG . (v . (x. 3)) = F . (v . (x. 3)) ) & ( M,v |= 'not' H implies FG . (v . (x. 3)) = G . (v . (x. 3)) ) ) ; :: thesis: FG is_definable_in M
rng FG c= M

proof

set v = the Function of VAR,M;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng FG or a in M )
assume a in rng FG ; :: thesis: a in M
then consider b being object such that
A13: b in M and
A14: a = FG . b by A11, FUNCT_1:def 3;
reconsider b = b as Element of M by A13;
A15: ( M, the Function of VAR,M / ((x. 3),b) |= H or M, the Function of VAR,M / ((x. 3),b) |= 'not' H ) by ZF_MODEL:14;
( the Function of VAR,M / ((x. 3),b)) . (x. 3) = b by FUNCT_7:128;
then ( FG . b = (def_func (H1,M)) . b or FG . b = (def_func (H2,M)) . b ) by A5, A8, A12, A15;
hence a in M by A14; :: thesis: verum

end;

then reconsider f = FG as Function of M,M by A11, FUNCT_2:def 1, RELSET_1:4;
take I = (H '&' H1) 'or' (('not' H) '&' H2); :: according to ZFMODEL1:def 3 :: thesis: ( Free I c= {(x. 3),(x. 4)} & M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(I <=> ((x. 4) '=' (x. 0)))))))) & FG = def_func (I,M) )
A16: Free ('not' H) = Free H by ZF_LANG1:60;
Free (H '&' H1) = (Free H) \/ (Free H1) by ZF_LANG1:61;
then A17: Free (H '&' H1) c= {(x. 3),(x. 4)} by A3, A9, A2, A1, XBOOLE_1:13;
A18: not x. 0 in Free H2 by A6, Lm1, Lm2, TARSKI:def 2;
A19: not x. 0 in Free H1 by A3, Lm1, Lm2, TARSKI:def 2;
Free (('not' H) '&' H2) = (Free ('not' H)) \/ (Free H2) by ZF_LANG1:61;
then A20: Free (('not' H) '&' H2) c= {(x. 3),(x. 4)} by A6, A9, A16, A2, A1, XBOOLE_1:13;
A21: Free I = (Free (H '&' H1)) \/ (Free (('not' H) '&' H2)) by ZF_LANG1:63;
hence Free I c= {(x. 3),(x. 4)} by A17, A20, XBOOLE_1:8; :: thesis: ( M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(I <=> ((x. 4) '=' (x. 0)))))))) & FG = def_func (I,M) )
then A22: not x. 0 in Free I by Lm1, Lm2, TARSKI:def 2;

A23: now :: thesis: for v being Function of VAR,M holds M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(I <=> ((x. 4) '=' (x. 0))))))))

let v be Function of VAR,M; :: thesis: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(I <=> ((x. 4) '=' (x. 0))))))))

now :: thesis: for m3 being Element of M ex m being Element of M st
for m4 being Element of M holds
( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= I implies m4 = m ) & ( m4 = m implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= I ) )

let m3 be Element of M; :: thesis: ex m being Element of M st
for m4 being Element of M holds
( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= I implies m4 = m ) & ( m4 = m implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= I ) )
M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) by A4;
then consider m1 being Element of M such that
A24: for m4 being Element of M holds
( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H1 iff m4 = m1 ) by A19, Th19;
M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) by A7;
then consider m2 being Element of M such that
A25: for m4 being Element of M holds
( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H2 iff m4 = m2 ) by A18, Th19;
( ( not M,v / ((x. 3),m3) |= 'not' H & M,v / ((x. 3),m3) |= H ) or ( M,v / ((x. 3),m3) |= 'not' H & not M,v / ((x. 3),m3) |= H ) ) by ZF_MODEL:14;
then consider m being Element of M such that
A26: ( ( not M,v / ((x. 3),m3) |= 'not' H & M,v / ((x. 3),m3) |= H & m = m1 ) or ( M,v / ((x. 3),m3) |= 'not' H & m = m2 & not M,v / ((x. 3),m3) |= H ) ) ;
take m = m; :: thesis: for m4 being Element of M holds
( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= I implies m4 = m ) & ( m4 = m implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= I ) )
let m4 be Element of M; :: thesis: ( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= I implies m4 = m ) & ( m4 = m implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= I ) )
thus ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= I implies m4 = m ) :: thesis: ( m4 = m implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= I )

proof

assume M,(v / ((x. 3),m3)) / ((x. 4),m4) |= I ; :: thesis: m4 = m
then ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H '&' H1 or M,(v / ((x. 3),m3)) / ((x. 4),m4) |= ('not' H) '&' H2 ) by ZF_MODEL:17;
then ( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H & M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H1 ) or ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= 'not' H & M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H2 ) ) by ZF_MODEL:15;
hence m4 = m by A10, A16, A24, A25, A26, Th9; :: thesis: verum

end;

assume m4 = m ; :: thesis: M,(v / ((x. 3),m3)) / ((x. 4),m4) |= I
then ( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H & M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H1 ) or ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= 'not' H & M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H2 ) ) by A10, A16, A24, A25, A26, Th9;
then ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H '&' H1 or M,(v / ((x. 3),m3)) / ((x. 4),m4) |= ('not' H) '&' H2 ) by ZF_MODEL:15;
hence M,(v / ((x. 3),m3)) / ((x. 4),m4) |= I by ZF_MODEL:17; :: thesis: verum

end;

hence M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(I <=> ((x. 4) '=' (x. 0)))))))) by A22, Th19; :: thesis: verum

end;

hence A27: M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(I <=> ((x. 4) '=' (x. 0)))))))) ; :: thesis: FG = def_func (I,M)

now :: thesis: for a being Element of M holds f . a = (def_func (I,M)) . a

set v = the Function of VAR,M;
let a be Element of M; :: thesis: f . a = (def_func (I,M)) . a
set m4 = (def_func (I,M)) . a;
A28: M, the Function of VAR,M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(I <=> ((x. 4) '=' (x. 0)))))))) by A23;
def_func (I,M) = def_func' (I, the Function of VAR,M) by A21, A17, A20, A27, Th11, XBOOLE_1:8;
then M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= I by A22, A28, Th10;
then ( M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= H '&' H1 or M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= ('not' H) '&' H2 ) by ZF_MODEL:17;
then ( ( M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= H & M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= H1 & M, the Function of VAR,M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) & def_func (H1,M) = def_func' (H1, the Function of VAR,M) ) or ( M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= 'not' H & M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= H2 & M, the Function of VAR,M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func (H2,M) = def_func' (H2, the Function of VAR,M) ) ) by A3, A4, A6, A7, Th11, ZF_MODEL:15;
then A29: ( ( M, the Function of VAR,M / ((x. 3),a) |= H & (def_func (I,M)) . a = F . a ) or ( M, the Function of VAR,M / ((x. 3),a) |= 'not' H & (def_func (I,M)) . a = G . a ) ) by A5, A8, A10, A16, A19, A18, Th9, Th10;
( the Function of VAR,M / ((x. 3),a)) . (x. 3) = a by FUNCT_7:128;
hence f . a = (def_func (I,M)) . a by A12, A29; :: thesis: verum

end;

hence FG = def_func (I,M) by FUNCT_2:63; :: thesis: verum