let M be non empty set ; :: thesis: for H, H1, H2 being ZF-formula

for v being Function of VAR,M st {(x. 0),(x. 1),(x. 2)} misses Free H1 & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) & {(x. 0),(x. 1),(x. 2)} misses Free H2 & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & {(x. 0),(x. 1),(x. 2)} misses Free H & not x. 4 in Free H holds

for FG being Function st dom FG = M & ( for m being Element of M holds

( ( M,v / ((x. 3),m) |= H implies FG . m = (def_func' (H1,v)) . m ) & ( M,v / ((x. 3),m) |= 'not' H implies FG . m = (def_func' (H2,v)) . m ) ) ) holds

FG is_parametrically_definable_in M

let H, H1, H2 be ZF-formula; :: thesis: for v being Function of VAR,M st {(x. 0),(x. 1),(x. 2)} misses Free H1 & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) & {(x. 0),(x. 1),(x. 2)} misses Free H2 & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & {(x. 0),(x. 1),(x. 2)} misses Free H & not x. 4 in Free H holds

for FG being Function st dom FG = M & ( for m being Element of M holds

( ( M,v / ((x. 3),m) |= H implies FG . m = (def_func' (H1,v)) . m ) & ( M,v / ((x. 3),m) |= 'not' H implies FG . m = (def_func' (H2,v)) . m ) ) ) holds

FG is_parametrically_definable_in M

let v be Function of VAR,M; :: thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free H1 & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) & {(x. 0),(x. 1),(x. 2)} misses Free H2 & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & {(x. 0),(x. 1),(x. 2)} misses Free H & not x. 4 in Free H implies for FG being Function st dom FG = M & ( for m being Element of M holds

( ( M,v / ((x. 3),m) |= H implies FG . m = (def_func' (H1,v)) . m ) & ( M,v / ((x. 3),m) |= 'not' H implies FG . m = (def_func' (H2,v)) . m ) ) ) holds

FG is_parametrically_definable_in M )

assume that

A1: {(x. 0),(x. 1),(x. 2)} misses Free H1 and

A2: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) and

A3: {(x. 0),(x. 1),(x. 2)} misses Free H2 and

A4: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) and

A5: {(x. 0),(x. 1),(x. 2)} misses Free H and

A6: not x. 4 in Free H ; :: thesis: for FG being Function st dom FG = M & ( for m being Element of M holds

( ( M,v / ((x. 3),m) |= H implies FG . m = (def_func' (H1,v)) . m ) & ( M,v / ((x. 3),m) |= 'not' H implies FG . m = (def_func' (H2,v)) . m ) ) ) holds

FG is_parametrically_definable_in M

let FG be Function; :: thesis: ( dom FG = M & ( for m being Element of M holds

( ( M,v / ((x. 3),m) |= H implies FG . m = (def_func' (H1,v)) . m ) & ( M,v / ((x. 3),m) |= 'not' H implies FG . m = (def_func' (H2,v)) . m ) ) ) implies FG is_parametrically_definable_in M )

assume that

A7: dom FG = M and

A8: for m being Element of M holds

( ( M,v / ((x. 3),m) |= H implies FG . m = (def_func' (H1,v)) . m ) & ( M,v / ((x. 3),m) |= 'not' H implies FG . m = (def_func' (H2,v)) . m ) ) ; :: thesis: FG is_parametrically_definable_in M

rng FG c= M

A11: x. 0 in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def 1;

then A12: not x. 0 in Free H1 by A1, XBOOLE_0:3;

take p = (H '&' H1) 'or' (('not' H) '&' H2); :: according to ZFMODEL1:def 4 :: thesis: ex b_{1} being Element of K27(K28(VAR,M)) st

( {(x. 0),(x. 1),(x. 2)} misses Free p & M,b_{1} |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))))) & FG = def_func' (p,b_{1}) )

take v ; :: thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free p & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))))) & FG = def_func' (p,v) )

A13: Free ('not' H) = Free H by ZF_LANG1:60;

A19: not x. 0 in Free H2 by A3, A11, XBOOLE_0:3;

not x. 0 in Free H by A5, A11, XBOOLE_0:3;

then A20: not x. 0 in Free p by A14, A12, A19;

for v being Function of VAR,M st {(x. 0),(x. 1),(x. 2)} misses Free H1 & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) & {(x. 0),(x. 1),(x. 2)} misses Free H2 & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & {(x. 0),(x. 1),(x. 2)} misses Free H & not x. 4 in Free H holds

for FG being Function st dom FG = M & ( for m being Element of M holds

( ( M,v / ((x. 3),m) |= H implies FG . m = (def_func' (H1,v)) . m ) & ( M,v / ((x. 3),m) |= 'not' H implies FG . m = (def_func' (H2,v)) . m ) ) ) holds

FG is_parametrically_definable_in M

let H, H1, H2 be ZF-formula; :: thesis: for v being Function of VAR,M st {(x. 0),(x. 1),(x. 2)} misses Free H1 & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) & {(x. 0),(x. 1),(x. 2)} misses Free H2 & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & {(x. 0),(x. 1),(x. 2)} misses Free H & not x. 4 in Free H holds

for FG being Function st dom FG = M & ( for m being Element of M holds

( ( M,v / ((x. 3),m) |= H implies FG . m = (def_func' (H1,v)) . m ) & ( M,v / ((x. 3),m) |= 'not' H implies FG . m = (def_func' (H2,v)) . m ) ) ) holds

FG is_parametrically_definable_in M

let v be Function of VAR,M; :: thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free H1 & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) & {(x. 0),(x. 1),(x. 2)} misses Free H2 & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & {(x. 0),(x. 1),(x. 2)} misses Free H & not x. 4 in Free H implies for FG being Function st dom FG = M & ( for m being Element of M holds

( ( M,v / ((x. 3),m) |= H implies FG . m = (def_func' (H1,v)) . m ) & ( M,v / ((x. 3),m) |= 'not' H implies FG . m = (def_func' (H2,v)) . m ) ) ) holds

FG is_parametrically_definable_in M )

assume that

A1: {(x. 0),(x. 1),(x. 2)} misses Free H1 and

A2: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) and

A3: {(x. 0),(x. 1),(x. 2)} misses Free H2 and

A4: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) and

A5: {(x. 0),(x. 1),(x. 2)} misses Free H and

A6: not x. 4 in Free H ; :: thesis: for FG being Function st dom FG = M & ( for m being Element of M holds

( ( M,v / ((x. 3),m) |= H implies FG . m = (def_func' (H1,v)) . m ) & ( M,v / ((x. 3),m) |= 'not' H implies FG . m = (def_func' (H2,v)) . m ) ) ) holds

FG is_parametrically_definable_in M

let FG be Function; :: thesis: ( dom FG = M & ( for m being Element of M holds

( ( M,v / ((x. 3),m) |= H implies FG . m = (def_func' (H1,v)) . m ) & ( M,v / ((x. 3),m) |= 'not' H implies FG . m = (def_func' (H2,v)) . m ) ) ) implies FG is_parametrically_definable_in M )

assume that

A7: dom FG = M and

A8: for m being Element of M holds

( ( M,v / ((x. 3),m) |= H implies FG . m = (def_func' (H1,v)) . m ) & ( M,v / ((x. 3),m) |= 'not' H implies FG . m = (def_func' (H2,v)) . m ) ) ; :: thesis: FG is_parametrically_definable_in M

rng FG c= M

proof

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

A9: b in M and

A10: a = FG . b by A7, FUNCT_1:def 3;

reconsider b = b as Element of M by A9;

( M,v / ((x. 3),b) |= H or M,v / ((x. 3),b) |= 'not' H ) by ZF_MODEL:14;

then ( a = (def_func' (H1,v)) . b or a = (def_func' (H2,v)) . b ) by A8, A10;

hence a in M ; :: thesis: verum

end;assume a in rng FG ; :: thesis: a in M

then consider b being object such that

A9: b in M and

A10: a = FG . b by A7, FUNCT_1:def 3;

reconsider b = b as Element of M by A9;

( M,v / ((x. 3),b) |= H or M,v / ((x. 3),b) |= 'not' H ) by ZF_MODEL:14;

then ( a = (def_func' (H1,v)) . b or a = (def_func' (H2,v)) . b ) by A8, A10;

hence a in M ; :: thesis: verum

A11: x. 0 in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def 1;

then A12: not x. 0 in Free H1 by A1, XBOOLE_0:3;

take p = (H '&' H1) 'or' (('not' H) '&' H2); :: according to ZFMODEL1:def 4 :: thesis: ex b

( {(x. 0),(x. 1),(x. 2)} misses Free p & M,b

take v ; :: thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free p & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))))) & FG = def_func' (p,v) )

A13: Free ('not' H) = Free H by ZF_LANG1:60;

A14: now :: thesis: for x being set holds

( not x in Free p or x in Free H or x in Free H1 or x in Free H2 )

( not x in Free p or x in Free H or x in Free H1 or x in Free H2 )

let x be set ; :: thesis: ( not x in Free p or x in Free H or x in Free H1 or x in Free H2 )

A15: Free (('not' H) '&' H2) = (Free ('not' H)) \/ (Free H2) by ZF_LANG1:61;

assume x in Free p ; :: thesis: ( x in Free H or x in Free H1 or x in Free H2 )

then x in (Free (H '&' H1)) \/ (Free (('not' H) '&' H2)) by ZF_LANG1:63;

then A16: ( x in Free (H '&' H1) or x in Free (('not' H) '&' H2) ) by XBOOLE_0:def 3;

Free (H '&' H1) = (Free H) \/ (Free H1) by ZF_LANG1:61;

hence ( x in Free H or x in Free H1 or x in Free H2 ) by A13, A16, A15, XBOOLE_0:def 3; :: thesis: verum

end;A15: Free (('not' H) '&' H2) = (Free ('not' H)) \/ (Free H2) by ZF_LANG1:61;

assume x in Free p ; :: thesis: ( x in Free H or x in Free H1 or x in Free H2 )

then x in (Free (H '&' H1)) \/ (Free (('not' H) '&' H2)) by ZF_LANG1:63;

then A16: ( x in Free (H '&' H1) or x in Free (('not' H) '&' H2) ) by XBOOLE_0:def 3;

Free (H '&' H1) = (Free H) \/ (Free H1) by ZF_LANG1:61;

hence ( x in Free H or x in Free H1 or x in Free H2 ) by A13, A16, A15, XBOOLE_0:def 3; :: thesis: verum

now :: thesis: for a being object st a in {(x. 0),(x. 1),(x. 2)} holds

not a in Free p

hence
{(x. 0),(x. 1),(x. 2)} misses Free p
by XBOOLE_0:3; :: thesis: ( M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))))) & FG = def_func' (p,v) )not a in Free p

let a be object ; :: thesis: ( a in {(x. 0),(x. 1),(x. 2)} implies not a in Free p )

assume that

A17: a in {(x. 0),(x. 1),(x. 2)} and

A18: a in Free p ; :: thesis: contradiction

( a in Free H or a in Free H1 or a in Free H2 ) by A14, A18;

hence contradiction by A1, A3, A5, A17, XBOOLE_0:3; :: thesis: verum

end;assume that

A17: a in {(x. 0),(x. 1),(x. 2)} and

A18: a in Free p ; :: thesis: contradiction

( a in Free H or a in Free H1 or a in Free H2 ) by A14, A18;

hence contradiction by A1, A3, A5, A17, XBOOLE_0:3; :: thesis: verum

A19: not x. 0 in Free H2 by A3, A11, XBOOLE_0:3;

not x. 0 in Free H by A5, A11, XBOOLE_0:3;

then A20: not x. 0 in Free p by A14, A12, A19;

now :: thesis: for m3 being Element of M ex r being Element of M st

for m4 being Element of M holds

( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p implies m4 = r ) & ( m4 = r implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p ) )

hence A24:
M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0))))))))
by A20, Th19; :: thesis: FG = def_func' (p,v)for m4 being Element of M holds

( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p implies m4 = r ) & ( m4 = r implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p ) )

let m3 be Element of M; :: thesis: ex r being Element of M st

for m4 being Element of M holds

( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p implies m4 = r ) & ( m4 = r implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p ) )

consider r1 being Element of M such that

A21: for m4 being Element of M holds

( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H1 iff m4 = r1 ) by A2, A12, Th19;

consider r2 being Element of M such that

A22: for m4 being Element of M holds

( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H2 iff m4 = r2 ) by A4, A19, Th19;

( ( M,v / ((x. 3),m3) |= H & not M,v / ((x. 3),m3) |= 'not' H ) or ( not M,v / ((x. 3),m3) |= H & M,v / ((x. 3),m3) |= 'not' H ) ) by ZF_MODEL:14;

then consider r being Element of M such that

A23: ( ( M,v / ((x. 3),m3) |= H & not M,v / ((x. 3),m3) |= 'not' H & r = r1 ) or ( not M,v / ((x. 3),m3) |= H & M,v / ((x. 3),m3) |= 'not' H & r = r2 ) ) ;

take r = r; :: thesis: for m4 being Element of M holds

( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p implies m4 = r ) & ( m4 = r implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p ) )

let m4 be Element of M; :: thesis: ( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p implies m4 = r ) & ( m4 = r implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p ) )

thus ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p implies m4 = r ) :: thesis: ( m4 = r implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p )

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 A6, A13, A21, A22, A23, 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) |= p by ZF_MODEL:17; :: thesis: verum

end;for m4 being Element of M holds

( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p implies m4 = r ) & ( m4 = r implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p ) )

consider r1 being Element of M such that

A21: for m4 being Element of M holds

( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H1 iff m4 = r1 ) by A2, A12, Th19;

consider r2 being Element of M such that

A22: for m4 being Element of M holds

( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H2 iff m4 = r2 ) by A4, A19, Th19;

( ( M,v / ((x. 3),m3) |= H & not M,v / ((x. 3),m3) |= 'not' H ) or ( not M,v / ((x. 3),m3) |= H & M,v / ((x. 3),m3) |= 'not' H ) ) by ZF_MODEL:14;

then consider r being Element of M such that

A23: ( ( M,v / ((x. 3),m3) |= H & not M,v / ((x. 3),m3) |= 'not' H & r = r1 ) or ( not M,v / ((x. 3),m3) |= H & M,v / ((x. 3),m3) |= 'not' H & r = r2 ) ) ;

take r = r; :: thesis: for m4 being Element of M holds

( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p implies m4 = r ) & ( m4 = r implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p ) )

let m4 be Element of M; :: thesis: ( ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p implies m4 = r ) & ( m4 = r implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p ) )

thus ( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p implies m4 = r ) :: thesis: ( m4 = r implies M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p )

proof

assume
m4 = r
; :: thesis: M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p
assume
M,(v / ((x. 3),m3)) / ((x. 4),m4) |= p
; :: thesis: m4 = r

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 = r by A6, A13, A21, A22, A23, 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 = r by A6, A13, A21, A22, A23, 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 A6, A13, A21, A22, A23, 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) |= p by ZF_MODEL:17; :: thesis: verum

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

hence
FG = def_func' (p,v)
by FUNCT_2:63; :: thesis: verumlet a be Element of M; :: thesis: f . a = (def_func' (p,v)) . a

set r = (def_func' (p,v)) . a;

M,(v / ((x. 3),a)) / ((x. 4),((def_func' (p,v)) . a)) |= p by A20, A24, Th10;

then ( M,(v / ((x. 3),a)) / ((x. 4),((def_func' (p,v)) . a)) |= H '&' H1 or M,(v / ((x. 3),a)) / ((x. 4),((def_func' (p,v)) . a)) |= ('not' H) '&' H2 ) by ZF_MODEL:17;

then ( ( M,(v / ((x. 3),a)) / ((x. 4),((def_func' (p,v)) . a)) |= H & M,(v / ((x. 3),a)) / ((x. 4),((def_func' (p,v)) . a)) |= H1 ) or ( M,(v / ((x. 3),a)) / ((x. 4),((def_func' (p,v)) . a)) |= 'not' H & M,(v / ((x. 3),a)) / ((x. 4),((def_func' (p,v)) . a)) |= H2 ) ) by ZF_MODEL:15;

then ( ( M,v / ((x. 3),a) |= H & (def_func' (p,v)) . a = (def_func' (H1,v)) . a ) or ( M,v / ((x. 3),a) |= 'not' H & (def_func' (p,v)) . a = (def_func' (H2,v)) . a ) ) by A2, A4, A6, A13, A12, A19, Th9, Th10;

hence f . a = (def_func' (p,v)) . a by A8; :: thesis: verum

end;set r = (def_func' (p,v)) . a;

M,(v / ((x. 3),a)) / ((x. 4),((def_func' (p,v)) . a)) |= p by A20, A24, Th10;

then ( M,(v / ((x. 3),a)) / ((x. 4),((def_func' (p,v)) . a)) |= H '&' H1 or M,(v / ((x. 3),a)) / ((x. 4),((def_func' (p,v)) . a)) |= ('not' H) '&' H2 ) by ZF_MODEL:17;

then ( ( M,(v / ((x. 3),a)) / ((x. 4),((def_func' (p,v)) . a)) |= H & M,(v / ((x. 3),a)) / ((x. 4),((def_func' (p,v)) . a)) |= H1 ) or ( M,(v / ((x. 3),a)) / ((x. 4),((def_func' (p,v)) . a)) |= 'not' H & M,(v / ((x. 3),a)) / ((x. 4),((def_func' (p,v)) . a)) |= H2 ) ) by ZF_MODEL:15;

then ( ( M,v / ((x. 3),a) |= H & (def_func' (p,v)) . a = (def_func' (H1,v)) . a ) or ( M,v / ((x. 3),a) |= 'not' H & (def_func' (p,v)) . a = (def_func' (H2,v)) . a ) ) by A2, A4, A6, A13, A12, A19, Th9, Th10;

hence f . a = (def_func' (p,v)) . a by A8; :: thesis: verum