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 ((),(All ((x. 4),(H1 <=> ((x. 4) '=' ()))))))) 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 ((),(All ((x. 4),(H2 <=> ((x. 4) '=' ()))))))) 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 ;
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:
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 ;
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 ;
take I = (H '&' H1) 'or' (() '&' H2); :: according to ZFMODEL1:def 3 :: thesis: ( Free I c= {(x. 3),(x. 4)} & M |= All ((x. 3),(Ex ((),(All ((x. 4),(I <=> ((x. 4) '=' ()))))))) & FG = def_func (I,M) )
A16: Free () = 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 ;
A18: not x. 0 in Free H2 by ;
A19: not x. 0 in Free H1 by ;
Free (() '&' H2) = (Free ()) \/ (Free H2) by ZF_LANG1:61;
then A20: Free (() '&' H2) c= {(x. 3),(x. 4)} by ;
A21: Free I = (Free (H '&' H1)) \/ (Free (() '&' H2)) by ZF_LANG1:63;
hence Free I c= {(x. 3),(x. 4)} by ; :: thesis: ( M |= All ((x. 3),(Ex ((),(All ((x. 4),(I <=> ((x. 4) '=' ()))))))) & FG = def_func (I,M) )
then A22: not x. 0 in Free I by ;
A23: now :: thesis: for v being Function of VAR,M holds M,v |= All ((x. 3),(Ex ((),(All ((x. 4),(I <=> ((x. 4) '=' ())))))))
let v be Function of VAR,M; :: thesis: M,v |= All ((x. 3),(Ex ((),(All ((x. 4),(I <=> ((x. 4) '=' ())))))))
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 ((),(All ((x. 4),(H1 <=> ((x. 4) '=' ()))))))) 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 ;
M,v |= All ((x. 3),(Ex ((),(All ((x. 4),(H2 <=> ((x. 4) '=' ()))))))) 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 ;
( ( 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) |= () '&' 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) |= () '&' 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 ((),(All ((x. 4),(I <=> ((x. 4) '=' ()))))))) by ; :: thesis: verum
end;
hence A27: M |= All ((x. 3),(Ex ((),(All ((x. 4),(I <=> ((x. 4) '=' ()))))))) ; :: 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 ((),(All ((x. 4),(I <=> ((x. 4) '=' ()))))))) by A23;
def_func (I,M) = def_func' (I, the Function of VAR,M) by ;
then M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= I by ;
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)) |= () '&' 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 ((),(All ((x. 4),(H1 <=> ((x. 4) '=' ()))))))) & 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 ((),(All ((x. 4),(H2 <=> ((x. 4) '=' ()))))))) & def_func (H2,M) = def_func' (H2, the Function of VAR,M) ) ) by ;
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 ; :: thesis: verum
end;
hence FG = def_func (I,M) by FUNCT_2:63; :: thesis: verum