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

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;

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

then reconsider f = FG as Function of M,M by A11, FUNCT_2:def 1, RELSET_1:4;
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;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

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))))))))

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

end;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 ) )

hence
M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(I <=> ((x. 4) '=' (x. 0))))))))
by A22, Th19; :: thesis: verumfor 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 )

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;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
m4 = m
; :: thesis: M,(v / ((x. 3),m3)) / ((x. 4),m4) |= I
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;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

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

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

hence
FG = def_func (I,M)
by FUNCT_2:63; :: thesis: verumset 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;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