let M be non empty set ; for F, G being Function st F is_definable_in M & G is_definable_in M holds
F * G is_definable_in M
let F, G be Function; ( F is_definable_in M & G is_definable_in M implies F * G is_definable_in M )
set x0 = x. 0 ;
set x3 = x. 3;
set x4 = x. 4;
given H1 being ZF-formula such that A1:
Free H1 c= {(x. 3),(x. 4)}
and
A2:
M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 )))))
and
A3:
F = def_func H1,M
; ZFMODEL1:def 3 ( not G is_definable_in M or F * G is_definable_in M )
given H2 being ZF-formula such that A4:
Free H2 c= {(x. 3),(x. 4)}
and
A5:
M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 )))))
and
A6:
G = def_func H2,M
; ZFMODEL1:def 3 F * G is_definable_in M
reconsider F = F, G = G as Function of M,M by A3, A6;
consider x being Variable such that
A7:
not x in variables_in (All (x. 0 ),(x. 3),(x. 4),(H1 '&' H2))
by Th4;
A8:
variables_in (All (x. 0 ),(x. 3),(x. 4),(H1 '&' H2)) = (variables_in (H1 '&' H2)) \/ {(x. 0 ),(x. 3),(x. 4)}
by ZF_LANG1:162;
then A9:
not x in {(x. 0 ),(x. 3),(x. 4)}
by A7, XBOOLE_0:def 3;
then A10:
x <> x. 3
by ENUMSET1:def 1;
take H = Ex x,((H1 / (x. 3),x) '&' (H2 / (x. 4),x)); ZFMODEL1:def 3 ( Free H c= {(x. 3),(x. 4)} & M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) & F * G = def_func H,M )
thus A11:
Free H c= {(x. 3),(x. 4)}
( M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) & F * G = def_func H,M )proof
let a be
set ;
TARSKI:def 3 ( not a in Free H or a in {(x. 3),(x. 4)} )
assume
a in Free H
;
a in {(x. 3),(x. 4)}
then A12:
a in (Free ((H1 / (x. 3),x) '&' (H2 / (x. 4),x))) \ {x}
by ZF_LANG1:71;
then
a in Free ((H1 / (x. 3),x) '&' (H2 / (x. 4),x))
by XBOOLE_0:def 5;
then
a in (Free (H1 / (x. 3),x)) \/ (Free (H2 / (x. 4),x))
by ZF_LANG1:66;
then
( (
Free (H1 / (x. 3),x) c= ((Free H1) \ {(x. 3)}) \/ {x} &
a in Free (H1 / (x. 3),x) ) or (
Free (H2 / (x. 4),x) c= ((Free H2) \ {(x. 4)}) \/ {x} &
a in Free (H2 / (x. 4),x) ) )
by Th1, XBOOLE_0:def 3;
then A13:
( (
(Free H1) \ {(x. 3)} c= Free H1 &
a in ((Free H1) \ {(x. 3)}) \/ {x} ) or (
(Free H2) \ {(x. 4)} c= Free H2 &
a in ((Free H2) \ {(x. 4)}) \/ {x} ) )
by XBOOLE_1:36;
not
a in {x}
by A12, XBOOLE_0:def 5;
then
( (
(Free H1) \ {(x. 3)} c= {(x. 3),(x. 4)} &
a in (Free H1) \ {(x. 3)} ) or (
(Free H2) \ {(x. 4)} c= {(x. 3),(x. 4)} &
a in (Free H2) \ {(x. 4)} ) )
by A1, A4, A13, XBOOLE_0:def 3, XBOOLE_1:1;
hence
a in {(x. 3),(x. 4)}
;
verum
end;
A14:
x. 0 <> x. 4
by ZF_LANG1:86;
A15:
x. 3 <> x. 4
by ZF_LANG1:86;
A16:
x <> x. 4
by A9, ENUMSET1:def 1;
variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2)
by ZF_LANG1:154;
then A17:
not x in (variables_in H1) \/ (variables_in H2)
by A7, A8, XBOOLE_0:def 3;
then A18:
not x in variables_in H1
by XBOOLE_0:def 3;
A19:
not x in variables_in H2
by A17, XBOOLE_0:def 3;
A20:
x. 0 <> x. 3
by ZF_LANG1:86;
then A21:
not x. 0 in Free H2
by A4, A14, TARSKI:def 2;
thus A22:
M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))))
F * G = def_func H,Mproof
let v be
Function of
VAR ,
M;
ZF_MODEL:def 5 M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))))
now let m3 be
Element of
M;
M,v / (x. 3),m3 |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))
M,
v |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 )))))
by A5, ZF_MODEL:def 5;
then
M,
v / (x. 3),
m3 |= Ex (x. 0 ),
(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 ))))
by ZF_LANG1:80;
then consider m0 being
Element of
M such that A23:
M,
(v / (x. 3),m3) / (x. 0 ),
m0 |= All (x. 4),
(H2 <=> ((x. 4) '=' (x. 0 )))
by ZF_LANG1:82;
M,
v |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 )))))
by A2, ZF_MODEL:def 5;
then
M,
v / (x. 3),
m0 |= Ex (x. 0 ),
(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))))
by ZF_LANG1:80;
then consider m being
Element of
M such that A24:
M,
(v / (x. 3),m0) / (x. 0 ),
m |= All (x. 4),
(H1 <=> ((x. 4) '=' (x. 0 )))
by ZF_LANG1:82;
now let m4 be
Element of
M;
M,((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4 |= H <=> ((x. 4) '=' (x. 0 ))A25:
now assume
M,
((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= H
;
M,((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4 |= (x. 4) '=' (x. 0 )then consider m9 being
Element of
M such that A26:
M,
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,
m9 |= (H1 / (x. 3),x) '&' (H2 / (x. 4),x)
by ZF_LANG1:82;
set v9 =
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,
m9;
A27:
((((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,m9) . x = m9
by FUNCT_7:130;
A28:
((((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,m9) / (x. 4),
m9 =
(((v / (x. 3),m3) / (x. 0 ),m) / x,m9) / (x. 4),
m9
by Th9
.=
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m9) / x,
m9
by A16, FUNCT_7:35
;
M,
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,
m9 |= H2 / (x. 4),
x
by A26, ZF_MODEL:15;
then
M,
((((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,m9) / (x. 4),
m9 |= H2
by A19, A27, Th13;
then A29:
M,
((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m9 |= H2
by A19, A28, Th6;
A30:
((v / (x. 3),m3) / (x. 4),m9) / (x. 0 ),
m0 = (((v / (x. 3),m3) / (x. 4),m9) / (x. 0 ),m) / (x. 0 ),
m0
by FUNCT_7:36;
A31:
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) . (x. 0 ) = ((v / (x. 3),m3) / (x. 0 ),m) . (x. 0 )
by FUNCT_7:34, ZF_LANG1:86;
A32:
(((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),m4) . (x. 0 ) = ((v / (x. 3),m0) / (x. 0 ),m) . (x. 0 )
by FUNCT_7:34, ZF_LANG1:86;
M,
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,
m9 |= H1 / (x. 3),
x
by A26, ZF_MODEL:15;
then A33:
M,
((((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,m9) / (x. 3),
m9 |= H1
by A18, A27, Th13;
A34:
((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),
m9 = ((v / (x. 3),m3) / (x. 4),m9) / (x. 0 ),
m0
by FUNCT_7:35, ZF_LANG1:86;
A35:
M,
((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),
m9 |= H2 <=> ((x. 4) '=' (x. 0 ))
by A23, ZF_LANG1:80;
A36:
(((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),m9) . (x. 0 ) = ((v / (x. 3),m3) / (x. 0 ),m0) . (x. 0 )
by FUNCT_7:34, ZF_LANG1:86;
((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m9 = ((v / (x. 3),m3) / (x. 4),m9) / (x. 0 ),
m
by FUNCT_7:35, ZF_LANG1:86;
then
M,
((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),
m9 |= H2
by A21, A30, A34, A29, Th10;
then
M,
((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),
m9 |= (x. 4) '=' (x. 0 )
by A35, ZF_MODEL:19;
then A37:
(((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),m9) . (x. 4) = (((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),m9) . (x. 0 )
by ZF_MODEL:12;
A38:
((v / (x. 3),m3) / (x. 0 ),m0) . (x. 0 ) = m0
by FUNCT_7:130;
(((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),m9) . (x. 4) = m9
by FUNCT_7:130;
then ((((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,m9) / (x. 3),
m9 =
((((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / (x. 3),m0) / x,
m9
by A10, A37, A38, A36, FUNCT_7:35
.=
(((v / (x. 0 ),m) / (x. 4),m4) / (x. 3),m0) / x,
m9
by Th9
.=
(((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),m4) / x,
m9
by A20, A14, A15, Th7
;
then A39:
M,
((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),
m4 |= H1
by A18, A33, Th6;
M,
((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),
m4 |= H1 <=> ((x. 4) '=' (x. 0 ))
by A24, ZF_LANG1:80;
then
M,
((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),
m4 |= (x. 4) '=' (x. 0 )
by A39, ZF_MODEL:19;
then A40:
(((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),m4) . (x. 4) = (((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),m4) . (x. 0 )
by ZF_MODEL:12;
A41:
((v / (x. 3),m0) / (x. 0 ),m) . (x. 0 ) = m
by FUNCT_7:130;
A42:
((v / (x. 3),m3) / (x. 0 ),m) . (x. 0 ) = m
by FUNCT_7:130;
A43:
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) . (x. 4) = m4
by FUNCT_7:130;
(((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),m4) . (x. 4) = m4
by FUNCT_7:130;
hence
M,
((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= (x. 4) '=' (x. 0 )
by A40, A41, A43, A42, A32, A31, ZF_MODEL:12;
verum end; now set v9 =
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,
m0;
A44:
((v / (x. 3),m0) / (x. 0 ),m) . (x. 0 ) = m
by FUNCT_7:130;
A45:
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) . (x. 4) = m4
by FUNCT_7:130;
A46:
M,
((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),
m0 |= H2 <=> ((x. 4) '=' (x. 0 ))
by A23, ZF_LANG1:80;
A47:
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) . (x. 0 ) = ((v / (x. 3),m3) / (x. 0 ),m) . (x. 0 )
by FUNCT_7:34, ZF_LANG1:86;
assume
M,
((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= (x. 4) '=' (x. 0 )
;
M,((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4 |= Hthen A48:
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) . (x. 4) = (((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) . (x. 0 )
by ZF_MODEL:12;
A49:
((v / (x. 3),m3) / (x. 0 ),m) . (x. 0 ) = m
by FUNCT_7:130;
A50:
(((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),m0) . (x. 0 ) = ((v / (x. 3),m3) / (x. 0 ),m0) . (x. 0 )
by FUNCT_7:34, ZF_LANG1:86;
A51:
M,
((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),
m4 |= H1 <=> ((x. 4) '=' (x. 0 ))
by A24, ZF_LANG1:80;
A52:
(((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),m4) . (x. 0 ) = ((v / (x. 3),m0) / (x. 0 ),m) . (x. 0 )
by FUNCT_7:34, ZF_LANG1:86;
(((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),m4) . (x. 4) = m4
by FUNCT_7:130;
then
M,
((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),
m4 |= (x. 4) '=' (x. 0 )
by A48, A44, A45, A49, A52, A47, ZF_MODEL:12;
then
M,
((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),
m4 |= H1
by A51, ZF_MODEL:19;
then A53:
M,
(((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),m4) / x,
m0 |= H1
by A18, Th6;
A54:
((v / (x. 3),m3) / (x. 0 ),m0) . (x. 0 ) = m0
by FUNCT_7:130;
(((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),m0) . (x. 4) = m0
by FUNCT_7:130;
then
M,
((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),
m0 |= (x. 4) '=' (x. 0 )
by A54, A50, ZF_MODEL:12;
then
M,
((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),
m0 |= H2
by A46, ZF_MODEL:19;
then A55:
M,
(((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),m0) / (x. 0 ),
m |= H2
by A21, Th10;
A56:
((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m0 = ((v / (x. 3),m3) / (x. 4),m0) / (x. 0 ),
m
by FUNCT_7:35, ZF_LANG1:86;
(((v / (x. 3),m3) / (x. 0 ),m0) / (x. 4),m0) / (x. 0 ),
m = ((v / (x. 3),m3) / (x. 4),m0) / (x. 0 ),
m
by Th9;
then A57:
M,
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m0) / x,
m0 |= H2
by A19, A55, A56, Th6;
A58:
((((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,m0) . x = m0
by FUNCT_7:130;
((((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,m0) / (x. 3),
m0 =
((((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / (x. 3),m0) / x,
m0
by A10, FUNCT_7:35
.=
(((v / (x. 0 ),m) / (x. 4),m4) / (x. 3),m0) / x,
m0
by Th9
.=
(((v / (x. 3),m0) / (x. 0 ),m) / (x. 4),m4) / x,
m0
by A20, A14, A15, Th7
;
then A59:
M,
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,
m0 |= H1 / (x. 3),
x
by A18, A53, A58, Th13;
((((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,m0) / (x. 4),
m0 =
(((v / (x. 3),m3) / (x. 0 ),m) / x,m0) / (x. 4),
m0
by Th9
.=
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m0) / x,
m0
by A16, FUNCT_7:35
;
then
M,
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,
m0 |= H2 / (x. 4),
x
by A19, A57, A58, Th13;
then
M,
(((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),m4) / x,
m0 |= (H1 / (x. 3),x) '&' (H2 / (x. 4),x)
by A59, ZF_MODEL:15;
hence
M,
((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= H
by ZF_LANG1:82;
verum end; hence
M,
((v / (x. 3),m3) / (x. 0 ),m) / (x. 4),
m4 |= H <=> ((x. 4) '=' (x. 0 ))
by A25, ZF_MODEL:19;
verum end; then
M,
(v / (x. 3),m3) / (x. 0 ),
m |= All (x. 4),
(H <=> ((x. 4) '=' (x. 0 )))
by ZF_LANG1:80;
hence
M,
v / (x. 3),
m3 |= Ex (x. 0 ),
(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))
by ZF_LANG1:82;
verum end;
hence
M,
v |= All (x. 3),
(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))))
by ZF_LANG1:80;
verum
end;
now let v be
Function of
VAR ,
M;
( ( M,v |= H implies (F * G) . (v . (x. 3)) = v . (x. 4) ) & ( (F * G) . (v . (x. 3)) = v . (x. 4) implies M,v |= H ) )thus
(
M,
v |= H implies
(F * G) . (v . (x. 3)) = v . (x. 4) )
( (F * G) . (v . (x. 3)) = v . (x. 4) implies M,v |= H )proof
assume
M,
v |= H
;
(F * G) . (v . (x. 3)) = v . (x. 4)
then consider m being
Element of
M such that A60:
M,
v / x,
m |= (H1 / (x. 3),x) '&' (H2 / (x. 4),x)
by ZF_LANG1:82;
A61:
(v / x,m) . x = m
by FUNCT_7:130;
M,
v / x,
m |= H1 / (x. 3),
x
by A60, ZF_MODEL:15;
then
M,
(v / x,m) / (x. 3),
m |= H1
by A18, A61, Th13;
then A62:
F . (((v / x,m) / (x. 3),m) . (x. 3)) = ((v / x,m) / (x. 3),m) . (x. 4)
by A1, A2, A3, ZFMODEL1:def 2;
A63:
((v / x,m) / (x. 3),m) . (x. 3) = m
by FUNCT_7:130;
A64:
((v / x,m) / (x. 4),m) . (x. 3) = (v / x,m) . (x. 3)
by FUNCT_7:34, ZF_LANG1:86;
A65:
v . (x. 3) = (v / x,m) . (x. 3)
by A10, FUNCT_7:34;
A66:
((v / x,m) / (x. 3),m) . (x. 4) = (v / x,m) . (x. 4)
by FUNCT_7:34, ZF_LANG1:86;
M,
v / x,
m |= H2 / (x. 4),
x
by A60, ZF_MODEL:15;
then
M,
(v / x,m) / (x. 4),
m |= H2
by A19, A61, Th13;
then A67:
G . (((v / x,m) / (x. 4),m) . (x. 3)) = ((v / x,m) / (x. 4),m) . (x. 4)
by A4, A5, A6, ZFMODEL1:def 2;
A68:
((v / x,m) / (x. 4),m) . (x. 4) = m
by FUNCT_7:130;
v . (x. 4) = (v / x,m) . (x. 4)
by A16, FUNCT_7:34;
hence
(F * G) . (v . (x. 3)) = v . (x. 4)
by A62, A63, A67, A68, A66, A64, A65, FUNCT_2:21;
verum
end; set m =
G . (v . (x. 3));
A69:
(v / (x. 4),(G . (v . (x. 3)))) . (x. 4) = G . (v . (x. 3))
by FUNCT_7:130;
A70:
(v / x,(G . (v . (x. 3)))) . x = G . (v . (x. 3))
by FUNCT_7:130;
A71:
(v / x,(G . (v . (x. 3)))) / (x. 4),
(G . (v . (x. 3))) = (v / (x. 4),(G . (v . (x. 3)))) / x,
(G . (v . (x. 3)))
by A16, FUNCT_7:35;
(v / (x. 4),(G . (v . (x. 3)))) . (x. 3) = v . (x. 3)
by FUNCT_7:34, ZF_LANG1:86;
then
M,
v / (x. 4),
(G . (v . (x. 3))) |= H2
by A4, A5, A6, A69, ZFMODEL1:def 2;
then
M,
(v / x,(G . (v . (x. 3)))) / (x. 4),
(G . (v . (x. 3))) |= H2
by A19, A71, Th6;
then A72:
M,
v / x,
(G . (v . (x. 3))) |= H2 / (x. 4),
x
by A19, A70, Th13;
A73:
(v / (x. 3),(G . (v . (x. 3)))) . (x. 3) = G . (v . (x. 3))
by FUNCT_7:130;
assume
(F * G) . (v . (x. 3)) = v . (x. 4)
;
M,v |= Hthen A74:
F . (G . (v . (x. 3))) = v . (x. 4)
by FUNCT_2:21;
A75:
(v / x,(G . (v . (x. 3)))) / (x. 3),
(G . (v . (x. 3))) = (v / (x. 3),(G . (v . (x. 3)))) / x,
(G . (v . (x. 3)))
by A10, FUNCT_7:35;
(v / (x. 3),(G . (v . (x. 3)))) . (x. 4) = v . (x. 4)
by FUNCT_7:34, ZF_LANG1:86;
then
M,
v / (x. 3),
(G . (v . (x. 3))) |= H1
by A1, A2, A3, A74, A73, ZFMODEL1:def 2;
then
M,
(v / x,(G . (v . (x. 3)))) / (x. 3),
(G . (v . (x. 3))) |= H1
by A18, A75, Th6;
then
M,
v / x,
(G . (v . (x. 3))) |= H1 / (x. 3),
x
by A18, A70, Th13;
then
M,
v / x,
(G . (v . (x. 3))) |= (H1 / (x. 3),x) '&' (H2 / (x. 4),x)
by A72, ZF_MODEL:15;
hence
M,
v |= H
by ZF_LANG1:82;
verum end;
hence
F * G = def_func H,M
by A11, A22, ZFMODEL1:def 2; verum