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 Th3;
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:149;
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
object ;
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:66;
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:61;
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;
hence
a in {(x. 3),(x. 4)}
;
verum
end;
A14:
x. 0 <> x. 4
by ZF_LANG1:76;
A15:
x. 3 <> x. 4
by ZF_LANG1:76;
A16:
x <> x. 4
by A9, ENUMSET1:def 1;
variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2)
by ZF_LANG1:141;
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:76;
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,M)proof
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 for m3 being Element of M holds M,v / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))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;
then
M,
v / (
(x. 3),
m3)
|= Ex (
(x. 0),
(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0))))))
by ZF_LANG1:71;
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:73;
M,
v |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))
by A2;
then
M,
v / (
(x. 3),
m0)
|= Ex (
(x. 0),
(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))
by ZF_LANG1:71;
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:73;
now for m4 being Element of M holds M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0))let m4 be
Element of
M;
M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0))A25:
now ( M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H implies M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) )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:73;
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:128;
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 Th8
.=
(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m9)) / (
x,
m9)
by A16, FUNCT_7:33
;
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, Th12;
then A29:
M,
((v / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m9)
|= H2
by A19, A28, Th5;
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:34;
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:32, ZF_LANG1:76;
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:32, ZF_LANG1:76;
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, Th12;
A34:
((v / ((x. 3),m3)) / ((x. 0),m0)) / (
(x. 4),
m9)
= ((v / ((x. 3),m3)) / ((x. 4),m9)) / (
(x. 0),
m0)
by FUNCT_7:33, ZF_LANG1:76;
A35:
M,
((v / ((x. 3),m3)) / ((x. 0),m0)) / (
(x. 4),
m9)
|= H2 <=> ((x. 4) '=' (x. 0))
by A23, ZF_LANG1:71;
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:32, ZF_LANG1:76;
((v / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m9)
= ((v / ((x. 3),m3)) / ((x. 4),m9)) / (
(x. 0),
m)
by FUNCT_7:33, ZF_LANG1:76;
then
M,
((v / ((x. 3),m3)) / ((x. 0),m0)) / (
(x. 4),
m9)
|= H2
by A21, A30, A34, A29, Th9;
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:128;
(((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m9)) . (x. 4) = m9
by FUNCT_7:128;
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:33
.=
(((v / ((x. 0),m)) / ((x. 4),m4)) / ((x. 3),m0)) / (
x,
m9)
by Th8
.=
(((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4)) / (
x,
m9)
by A20, A14, A15, Th6
;
then A39:
M,
((v / ((x. 3),m0)) / ((x. 0),m)) / (
(x. 4),
m4)
|= H1
by A18, A33, Th5;
M,
((v / ((x. 3),m0)) / ((x. 0),m)) / (
(x. 4),
m4)
|= H1 <=> ((x. 4) '=' (x. 0))
by A24, ZF_LANG1:71;
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:128;
A42:
((v / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) = m
by FUNCT_7:128;
A43:
(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = m4
by FUNCT_7:128;
(((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = m4
by FUNCT_7:128;
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 ( M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) implies M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H )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:128;
A45:
(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = m4
by FUNCT_7:128;
A46:
M,
((v / ((x. 3),m3)) / ((x. 0),m0)) / (
(x. 4),
m0)
|= H2 <=> ((x. 4) '=' (x. 0))
by A23, ZF_LANG1:71;
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:32, ZF_LANG1:76;
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:128;
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:32, ZF_LANG1:76;
A51:
M,
((v / ((x. 3),m0)) / ((x. 0),m)) / (
(x. 4),
m4)
|= H1 <=> ((x. 4) '=' (x. 0))
by A24, ZF_LANG1:71;
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:32, ZF_LANG1:76;
(((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = m4
by FUNCT_7:128;
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, Th5;
A54:
((v / ((x. 3),m3)) / ((x. 0),m0)) . (x. 0) = m0
by FUNCT_7:128;
(((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m0)) . (x. 4) = m0
by FUNCT_7:128;
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, Th9;
A56:
((v / ((x. 3),m3)) / ((x. 0),m)) / (
(x. 4),
m0)
= ((v / ((x. 3),m3)) / ((x. 4),m0)) / (
(x. 0),
m)
by FUNCT_7:33, ZF_LANG1:76;
(((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m0)) / (
(x. 0),
m)
= ((v / ((x. 3),m3)) / ((x. 4),m0)) / (
(x. 0),
m)
by Th8;
then A57:
M,
(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m0)) / (
x,
m0)
|= H2
by A19, A55, A56, Th5;
A58:
((((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m0)) . x = m0
by FUNCT_7:128;
((((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:33
.=
(((v / ((x. 0),m)) / ((x. 4),m4)) / ((x. 3),m0)) / (
x,
m0)
by Th8
.=
(((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4)) / (
x,
m0)
by A20, A14, A15, Th6
;
then A59:
M,
(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (
x,
m0)
|= H1 / (
(x. 3),
x)
by A18, A53, A58, Th12;
((((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 Th8
.=
(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m0)) / (
x,
m0)
by A16, FUNCT_7:33
;
then
M,
(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (
x,
m0)
|= H2 / (
(x. 4),
x)
by A19, A57, A58, Th12;
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:73;
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:71;
hence
M,
v / (
(x. 3),
m3)
|= Ex (
(x. 0),
(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))
by ZF_LANG1:73;
verum end;
hence
M,
v |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))
by ZF_LANG1:71;
verum
end;
now for v being Function of VAR,M holds
( ( M,v |= H implies (F * G) . (v . (x. 3)) = v . (x. 4) ) & ( (F * G) . (v . (x. 3)) = v . (x. 4) implies M,v |= H ) )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:73;
A61:
(v / (x,m)) . x = m
by FUNCT_7:128;
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, Th12;
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:128;
A64:
((v / (x,m)) / ((x. 4),m)) . (x. 3) = (v / (x,m)) . (x. 3)
by FUNCT_7:32, ZF_LANG1:76;
A65:
v . (x. 3) = (v / (x,m)) . (x. 3)
by A10, FUNCT_7:32;
A66:
((v / (x,m)) / ((x. 3),m)) . (x. 4) = (v / (x,m)) . (x. 4)
by FUNCT_7:32, ZF_LANG1:76;
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, Th12;
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:128;
v . (x. 4) = (v / (x,m)) . (x. 4)
by A16, FUNCT_7:32;
hence
(F * G) . (v . (x. 3)) = v . (x. 4)
by A62, A63, A67, A68, A66, A64, A65, FUNCT_2:15;
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:128;
A70:
(v / (x,(G . (v . (x. 3))))) . x = G . (v . (x. 3))
by FUNCT_7:128;
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:33;
(v / ((x. 4),(G . (v . (x. 3))))) . (x. 3) = v . (x. 3)
by FUNCT_7:32, ZF_LANG1:76;
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, Th5;
then A72:
M,
v / (
x,
(G . (v . (x. 3))))
|= H2 / (
(x. 4),
x)
by A19, A70, Th12;
A73:
(v / ((x. 3),(G . (v . (x. 3))))) . (x. 3) = G . (v . (x. 3))
by FUNCT_7:128;
assume
(F * G) . (v . (x. 3)) = v . (x. 4)
;
M,v |= Hthen A74:
F . (G . (v . (x. 3))) = v . (x. 4)
by FUNCT_2:15;
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:33;
(v / ((x. 3),(G . (v . (x. 3))))) . (x. 4) = v . (x. 4)
by FUNCT_7:32, ZF_LANG1:76;
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, Th5;
then
M,
v / (
x,
(G . (v . (x. 3))))
|= H1 / (
(x. 3),
x)
by A18, A70, Th12;
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:73;
verum end;
hence
F * G = def_func (H,M)
by A11, A22, ZFMODEL1:def 2; verum