let M be non empty set ; for F, G being Function st F is_parametrically_definable_in M & G is_parametrically_definable_in M holds
G * F is_parametrically_definable_in M
let F, G be Function; ( F is_parametrically_definable_in M & G is_parametrically_definable_in M implies G * F is_parametrically_definable_in M )
given H1 being ZF-formula, v1 being Function of VAR,M such that A1:
{(x. 0),(x. 1),(x. 2)} misses Free H1
and
A2:
M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))
and
A3:
F = def_func' (H1,v1)
; ZFMODEL1:def 4 ( not G is_parametrically_definable_in M or G * F is_parametrically_definable_in M )
given H2 being ZF-formula, v2 being Function of VAR,M such that A4:
{(x. 0),(x. 1),(x. 2)} misses Free H2
and
A5:
M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0))))))))
and
A6:
G = def_func' (H2,v2)
; ZFMODEL1:def 4 G * F is_parametrically_definable_in M
reconsider F9 = F, G9 = G as Function of M,M by A3, A6;
deffunc H1( object ) -> set = v2 . $1;
consider i being Element of NAT such that
A7:
for j being Element of NAT st x. j in variables_in H2 holds
j < i
by Th3;
( i > 4 or not i > 4 )
;
then consider i3 being Element of NAT such that
A8:
( ( i > 4 & i3 = i ) or ( not i > 4 & i3 = 5 ) )
;
A9:
x. 0 in {(x. 0),(x. 1),(x. 2)}
by ENUMSET1:def 1;
then
not x. 0 in Free H1
by A1, XBOOLE_0:3;
then consider H3 being ZF-formula, v3 being Function of VAR,M such that
A10:
for j being Element of NAT st j < i3 & x. j in variables_in H3 & not j = 3 holds
j = 4
and
A11:
not x. 0 in Free H3
and
A12:
M,v3 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H3 <=> ((x. 4) '=' (x. 0))))))))
and
A13:
def_func' (H1,v1) = def_func' (H3,v3)
by A2, Th16;
consider k1 being Element of NAT such that
A14:
for j being Element of NAT st x. j in variables_in H3 holds
j < k1
by Th3;
( k1 > i3 or k1 <= i3 )
;
then consider k being Element of NAT such that
A15:
( ( k1 > i3 & k = k1 ) or ( k1 <= i3 & k = i3 + 1 ) )
;
deffunc H2( object ) -> set = v3 . $1;
defpred S1[ object ] means $1 in Free H3;
take H = Ex ((x. k),((H3 / ((x. 4),(x. k))) '&' (H2 / ((x. 3),(x. k))))); ZFMODEL1:def 4 ex b1 being Element of K27(K28(VAR,M)) st
( {(x. 0),(x. 1),(x. 2)} misses Free H & M,b1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & G * F = def_func' (H,b1) )
consider v being Function such that
A16:
( dom v = VAR & ( for a being object st a in VAR holds
( ( S1[a] implies v . a = H2(a) ) & ( not S1[a] implies v . a = H1(a) ) ) ) )
from PARTFUN1:sch 1();
rng v c= M
then reconsider v = v as Function of VAR,M by A16, FUNCT_2:def 1, RELSET_1:4;
take
v
; ( {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & G * F = def_func' (H,v) )
A19:
{(x. 0),(x. 1),(x. 2)} misses Free H3
proof
A20:
i3 > 2
by A8, XXREAL_0:2;
A21:
i3 > 1
by A8, XXREAL_0:2;
assume
{(x. 0),(x. 1),(x. 2)} meets Free H3
;
contradiction
then consider a being
object such that A22:
a in {(x. 0),(x. 1),(x. 2)}
and A23:
a in Free H3
by XBOOLE_0:3;
A24:
Free H3 c= variables_in H3
by ZF_LANG1:151;
(
a = x. 0 or
a = x. 1 or
a = x. 2 )
by A22, ENUMSET1:def 1;
hence
contradiction
by A10, A21, A20, A23, A24;
verum
end;
A25:
now for a being object st a in {(x. 0),(x. 1),(x. 2)} holds
not a in Free Hlet a be
object ;
( a in {(x. 0),(x. 1),(x. 2)} implies not a in Free H )assume A26:
a in {(x. 0),(x. 1),(x. 2)}
;
not a in Free Hassume
a in Free H
;
contradictionthen A27:
a in (Free ((H3 / ((x. 4),(x. k))) '&' (H2 / ((x. 3),(x. k))))) \ {(x. k)}
by ZF_LANG1:66;
then A28:
not
a in {(x. k)}
by XBOOLE_0:def 5;
A29:
Free ((H3 / ((x. 4),(x. k))) '&' (H2 / ((x. 3),(x. k)))) = (Free (H3 / ((x. 4),(x. k)))) \/ (Free (H2 / ((x. 3),(x. k))))
by ZF_LANG1:61;
a in Free ((H3 / ((x. 4),(x. k))) '&' (H2 / ((x. 3),(x. k))))
by A27, XBOOLE_0:def 5;
then
( (
Free (H3 / ((x. 4),(x. k))) c= ((Free H3) \ {(x. 4)}) \/ {(x. k)} &
a in Free (H3 / ((x. 4),(x. k))) ) or (
a in Free (H2 / ((x. 3),(x. k))) &
Free (H2 / ((x. 3),(x. k))) c= ((Free H2) \ {(x. 3)}) \/ {(x. k)} ) )
by A29, Th1, XBOOLE_0:def 3;
then
(
a in (Free H3) \ {(x. 4)} or
a in (Free H2) \ {(x. 3)} )
by A28, XBOOLE_0:def 3;
then
(
a in Free H3 or
a in Free H2 )
by XBOOLE_0:def 5;
hence
contradiction
by A4, A19, A26, XBOOLE_0:3;
verum end;
hence
{(x. 0),(x. 1),(x. 2)} misses Free H
by XBOOLE_0:3; ( M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & G * F = def_func' (H,v) )
x. 0 in {(x. 0),(x. 1),(x. 2)}
by ENUMSET1:def 1;
then A30:
not x. 0 in Free H
by A25;
A31:
k <> 4
by A8, A15, NAT_1:13;
then A32:
x. k <> x. 4
by ZF_LANG1:76;
A33:
i <= i3
by A8, XXREAL_0:2;
A34:
not x. k in variables_in H2
A35:
for x being Variable holds
( not x in Free H2 or not x in Free H3 or x = x. 3 or x = x. 4 )
A40:
k <> 3
by A8, A15, NAT_1:13, XXREAL_0:2;
then A41:
x. k <> x. 3
by ZF_LANG1:76;
A42:
not x. k in variables_in H3
A43:
not x. 0 in Free H2
by A4, A9, XBOOLE_0:3;
now for m1 being Element of M ex r being Element of M st
for m3 being Element of M holds
( ( M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H implies m3 = r ) & ( m3 = r implies M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H ) )let m1 be
Element of
M;
ex r being Element of M st
for m3 being Element of M holds
( ( M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H implies m3 = r ) & ( m3 = r implies M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H ) )A44:
not
x. 3
in variables_in (H2 / ((x. 3),(x. k)))
by A40, ZF_LANG1:76, ZF_LANG1:184;
consider m being
Element of
M such that A45:
for
m4 being
Element of
M holds
(
M,
(v3 / ((x. 3),m1)) / (
(x. 4),
m4)
|= H3 iff
m4 = m )
by A11, A12, Th19;
A46:
now for x being Variable st x in Free (H3 / ((x. 4),(x. k))) holds
((v / ((x. 3),m1)) / ((x. k),m)) . x = ((v3 / ((x. 3),m1)) / ((x. k),m)) . xlet x be
Variable;
( x in Free (H3 / ((x. 4),(x. k))) implies ((v / ((x. 3),m1)) / ((x. k),m)) . x = ((v3 / ((x. 3),m1)) / ((x. k),m)) . x )assume A47:
x in Free (H3 / ((x. 4),(x. k)))
;
((v / ((x. 3),m1)) / ((x. k),m)) . x = ((v3 / ((x. 3),m1)) / ((x. k),m)) . x
Free (H3 / ((x. 4),(x. k))) c= ((Free H3) \ {(x. 4)}) \/ {(x. k)}
by Th1;
then
(
x in (Free H3) \ {(x. 4)} or
x in {(x. k)} )
by A47, XBOOLE_0:def 3;
then
( (
x in Free H3 & not
x in {(x. 4)} ) or
x = x. k )
by TARSKI:def 1, XBOOLE_0:def 5;
then
( ( ( (
x in Free H3 &
x. 3
<> x &
x <> x. k ) or
x = x. 4 or
x = x. 3 ) &
x <> x. 4 ) or (
((v / ((x. 3),m1)) / ((x. k),m)) . x = m &
((v3 / ((x. 3),m1)) / ((x. k),m)) . x = m ) )
by FUNCT_7:128, TARSKI:def 1;
then
( (
((v / ((x. 3),m1)) / ((x. k),m)) . x = (v / ((x. 3),m1)) . x &
(v / ((x. 3),m1)) . x = v . x &
v . x = v3 . x &
v3 . x = (v3 / ((x. 3),m1)) . x &
(v3 / ((x. 3),m1)) . x = ((v3 / ((x. 3),m1)) / ((x. k),m)) . x ) or (
((v / ((x. 3),m1)) / ((x. k),m)) . x = (v / ((x. 3),m1)) . x &
(v / ((x. 3),m1)) . x = m1 &
m1 = (v3 / ((x. 3),m1)) . x &
(v3 / ((x. 3),m1)) . x = ((v3 / ((x. 3),m1)) / ((x. k),m)) . x ) or
((v / ((x. 3),m1)) / ((x. k),m)) . x = ((v3 / ((x. 3),m1)) / ((x. k),m)) . x )
by A41, A16, FUNCT_7:32, FUNCT_7:128;
hence
((v / ((x. 3),m1)) / ((x. k),m)) . x = ((v3 / ((x. 3),m1)) / ((x. k),m)) . x
;
verum end; consider r being
Element of
M such that A48:
for
m4 being
Element of
M holds
(
M,
(v2 / ((x. 3),m)) / (
(x. 4),
m4)
|= H2 iff
m4 = r )
by A5, A43, Th19;
take r =
r;
for m3 being Element of M holds
( ( M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H implies m3 = r ) & ( m3 = r implies M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H ) )let m3 be
Element of
M;
( ( M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H implies m3 = r ) & ( m3 = r implies M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H ) )A49:
((v3 / ((x. 3),m1)) / ((x. 4),m)) . (x. 4) = m
by FUNCT_7:128;
thus
(
M,
(v / ((x. 3),m1)) / (
(x. 4),
m3)
|= H implies
m3 = r )
( m3 = r implies M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H )proof
A50:
now for x being Variable st x in Free H2 holds
((v / ((x. 3),m)) / ((x. 4),m3)) . x = ((v2 / ((x. 3),m)) / ((x. 4),m3)) . xlet x be
Variable;
( x in Free H2 implies ((v / ((x. 3),m)) / ((x. 4),m3)) . x = ((v2 / ((x. 3),m)) / ((x. 4),m3)) . x )assume
x in Free H2
;
((v / ((x. 3),m)) / ((x. 4),m3)) . x = ((v2 / ((x. 3),m)) / ((x. 4),m3)) . xthen
( ( not
x in Free H3 &
x <> x. 3 &
x <> x. 4 ) or
x = x. 3 or
x = x. 4 )
by A35;
then
( (
((v / ((x. 3),m)) / ((x. 4),m3)) . x = (v / ((x. 3),m)) . x &
(v / ((x. 3),m)) . x = v . x &
v . x = v2 . x &
v2 . x = (v2 / ((x. 3),m)) . x &
(v2 / ((x. 3),m)) . x = ((v2 / ((x. 3),m)) / ((x. 4),m3)) . x ) or (
((v / ((x. 3),m)) / ((x. 4),m3)) . x = (v / ((x. 3),m)) . x &
(v / ((x. 3),m)) . x = m &
((v2 / ((x. 3),m)) / ((x. 4),m3)) . x = (v2 / ((x. 3),m)) . x &
(v2 / ((x. 3),m)) . x = m ) or (
((v / ((x. 3),m)) / ((x. 4),m3)) . x = m3 &
((v2 / ((x. 3),m)) / ((x. 4),m3)) . x = m3 ) )
by A16, Lm3, FUNCT_7:32, FUNCT_7:128;
hence
((v / ((x. 3),m)) / ((x. 4),m3)) . x = ((v2 / ((x. 3),m)) / ((x. 4),m3)) . x
;
verum end;
assume
M,
(v / ((x. 3),m1)) / (
(x. 4),
m3)
|= H
;
m3 = r
then consider n being
Element of
M such that A51:
M,
((v / ((x. 3),m1)) / ((x. 4),m3)) / (
(x. k),
n)
|= (H3 / ((x. 4),(x. k))) '&' (H2 / ((x. 3),(x. k)))
by ZF_LANG1:73;
A52:
now for x being Variable st x in Free H3 holds
((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . xlet x be
Variable;
( x in Free H3 implies ((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x )assume A53:
x in Free H3
;
((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . xA54:
((v / ((x. 3),m1)) / ((x. 4),n)) . (x. 4) = n
by FUNCT_7:128;
A55:
((v3 / ((x. 3),m1)) / ((x. 4),n)) . (x. 3) = (v3 / ((x. 3),m1)) . (x. 3)
by FUNCT_7:32, ZF_LANG1:76;
A56:
((v / ((x. 3),m1)) / ((x. 4),n)) . (x. 3) = (v / ((x. 3),m1)) . (x. 3)
by FUNCT_7:32, ZF_LANG1:76;
A57:
(v / ((x. 3),m1)) . (x. 3) = m1
by FUNCT_7:128;
(
x = x. 3 or
x = x. 4 or (
x <> x. 3 &
x <> x. 4 ) )
;
then
(
((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x or (
(v / ((x. 3),m1)) . x = v . x &
(v3 / ((x. 3),m1)) . x = v3 . x &
((v / ((x. 3),m1)) / ((x. 4),n)) . x = (v / ((x. 3),m1)) . x &
((v3 / ((x. 3),m1)) / ((x. 4),n)) . x = (v3 / ((x. 3),m1)) . x ) )
by A54, A57, A56, A55, FUNCT_7:32, FUNCT_7:128;
hence
((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x
by A16, A53;
verum end;
A58:
M,
((v / ((x. 3),m1)) / ((x. 4),m3)) / (
(x. k),
n)
|= H2 / (
(x. 3),
(x. k))
by A51, ZF_MODEL:15;
A59:
(((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. k),n)) . (x. k) = n
by FUNCT_7:128;
M,
((v / ((x. 3),m1)) / ((x. 4),m3)) / (
(x. k),
n)
|= H3 / (
(x. 4),
(x. k))
by A51, ZF_MODEL:15;
then
M,
(((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. k),n)) / (
(x. 4),
n)
|= H3
by A42, A59, Th12;
then
M,
((v / ((x. 3),m1)) / ((x. k),n)) / (
(x. 4),
n)
|= H3
by Th8;
then
M,
((v / ((x. 3),m1)) / ((x. 4),n)) / (
(x. k),
n)
|= H3
by A31, FUNCT_7:33, ZF_LANG1:76;
then
M,
(v / ((x. 3),m1)) / (
(x. 4),
n)
|= H3
by A42, Th5;
then
M,
(v3 / ((x. 3),m1)) / (
(x. 4),
n)
|= H3
by A52, ZF_LANG1:75;
then
n = m
by A45;
then
M,
(((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. k),m)) / (
(x. 3),
m)
|= H2
by A34, A59, A58, Th12;
then
M,
((v / ((x. 4),m3)) / ((x. k),m)) / (
(x. 3),
m)
|= H2
by Th8;
then
M,
((v / ((x. 3),m)) / ((x. 4),m3)) / (
(x. k),
m)
|= H2
by A41, A32, Lm3, Th6;
then
M,
(v / ((x. 3),m)) / (
(x. 4),
m3)
|= H2
by A34, Th5;
then
M,
(v2 / ((x. 3),m)) / (
(x. 4),
m3)
|= H2
by A50, ZF_LANG1:75;
hence
m3 = r
by A48;
verum
end; assume
m3 = r
;
M,(v / ((x. 3),m1)) / ((x. 4),m3) |= Hthen A60:
M,
(v2 / ((x. 3),m)) / (
(x. 4),
m3)
|= H2
by A48;
A61:
(v2 / ((x. 3),m)) . (x. 3) = m
by FUNCT_7:128;
A62:
now for x being Variable st x in Free (H2 / ((x. 3),(x. k))) holds
((v / ((x. 4),m3)) / ((x. k),m)) . x = ((v2 / ((x. 4),m3)) / ((x. k),m)) . xlet x be
Variable;
( x in Free (H2 / ((x. 3),(x. k))) implies ((v / ((x. 4),m3)) / ((x. k),m)) . x = ((v2 / ((x. 4),m3)) / ((x. k),m)) . x )assume A63:
x in Free (H2 / ((x. 3),(x. k)))
;
((v / ((x. 4),m3)) / ((x. k),m)) . x = ((v2 / ((x. 4),m3)) / ((x. k),m)) . x
Free (H2 / ((x. 3),(x. k))) c= ((Free H2) \ {(x. 3)}) \/ {(x. k)}
by Th1;
then
(
x in (Free H2) \ {(x. 3)} or
x in {(x. k)} )
by A63, XBOOLE_0:def 3;
then
( (
x in Free H2 & not
x in {(x. 3)} ) or
x = x. k )
by TARSKI:def 1, XBOOLE_0:def 5;
then
( ( ( ( not
x in Free H3 &
x. 4
<> x &
x <> x. k ) or
x = x. 3 or
x = x. 4 ) &
x <> x. 3 ) or (
((v / ((x. 4),m3)) / ((x. k),m)) . x = m &
((v2 / ((x. 4),m3)) / ((x. k),m)) . x = m ) )
by A35, FUNCT_7:128, TARSKI:def 1;
then
( (
((v / ((x. 4),m3)) / ((x. k),m)) . x = (v / ((x. 4),m3)) . x &
(v / ((x. 4),m3)) . x = v . x &
v . x = v2 . x &
v2 . x = (v2 / ((x. 4),m3)) . x &
(v2 / ((x. 4),m3)) . x = ((v2 / ((x. 4),m3)) / ((x. k),m)) . x ) or (
((v / ((x. 4),m3)) / ((x. k),m)) . x = (v / ((x. 4),m3)) . x &
(v / ((x. 4),m3)) . x = m3 &
m3 = (v2 / ((x. 4),m3)) . x &
(v2 / ((x. 4),m3)) . x = ((v2 / ((x. 4),m3)) / ((x. k),m)) . x ) or
((v / ((x. 4),m3)) / ((x. k),m)) . x = ((v2 / ((x. 4),m3)) / ((x. k),m)) . x )
by A32, A16, FUNCT_7:32, FUNCT_7:128;
hence
((v / ((x. 4),m3)) / ((x. k),m)) . x = ((v2 / ((x. 4),m3)) / ((x. k),m)) . x
;
verum end; A64:
not
x. 4
in variables_in (H3 / ((x. 4),(x. k)))
by A31, ZF_LANG1:76, ZF_LANG1:184;
M,
(v3 / ((x. 3),m1)) / (
(x. 4),
m)
|= H3
by A45;
then
M,
((v3 / ((x. 3),m1)) / ((x. 4),m)) / (
(x. k),
m)
|= H3 / (
(x. 4),
(x. k))
by A42, A49, Th13;
then
M,
((v3 / ((x. 3),m1)) / ((x. k),m)) / (
(x. 4),
m)
|= H3 / (
(x. 4),
(x. k))
by A31, FUNCT_7:33, ZF_LANG1:76;
then
M,
(v3 / ((x. 3),m1)) / (
(x. k),
m)
|= H3 / (
(x. 4),
(x. k))
by A64, Th5;
then
M,
(v / ((x. 3),m1)) / (
(x. k),
m)
|= H3 / (
(x. 4),
(x. k))
by A46, ZF_LANG1:75;
then
M,
((v / ((x. 3),m1)) / ((x. k),m)) / (
(x. 4),
m3)
|= H3 / (
(x. 4),
(x. k))
by A64, Th5;
then A65:
M,
((v / ((x. 3),m1)) / ((x. 4),m3)) / (
(x. k),
m)
|= H3 / (
(x. 4),
(x. k))
by A31, FUNCT_7:33, ZF_LANG1:76;
((v2 / ((x. 3),m)) / ((x. 4),m3)) . (x. 3) = (v2 / ((x. 3),m)) . (x. 3)
by FUNCT_7:32, ZF_LANG1:76;
then
M,
((v2 / ((x. 3),m)) / ((x. 4),m3)) / (
(x. k),
m)
|= H2 / (
(x. 3),
(x. k))
by A34, A61, A60, Th13;
then
M,
((v2 / ((x. 4),m3)) / ((x. k),m)) / (
(x. 3),
m)
|= H2 / (
(x. 3),
(x. k))
by A41, A32, Lm3, Th6;
then
M,
(v2 / ((x. 4),m3)) / (
(x. k),
m)
|= H2 / (
(x. 3),
(x. k))
by A44, Th5;
then
M,
(v / ((x. 4),m3)) / (
(x. k),
m)
|= H2 / (
(x. 3),
(x. k))
by A62, ZF_LANG1:75;
then
M,
((v / ((x. 4),m3)) / ((x. k),m)) / (
(x. 3),
m1)
|= H2 / (
(x. 3),
(x. k))
by A44, Th5;
then
M,
((v / ((x. 3),m1)) / ((x. 4),m3)) / (
(x. k),
m)
|= H2 / (
(x. 3),
(x. k))
by A41, A32, Lm3, Th6;
then
M,
((v / ((x. 3),m1)) / ((x. 4),m3)) / (
(x. k),
m)
|= (H3 / ((x. 4),(x. k))) '&' (H2 / ((x. 3),(x. k)))
by A65, ZF_MODEL:15;
hence
M,
(v / ((x. 3),m1)) / (
(x. 4),
m3)
|= H
by ZF_LANG1:73;
verum end;
hence A66:
M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))
by A30, Th19; G * F = def_func' (H,v)
now for a being object st a in M holds
(G9 * F9) . a = (def_func' (H,v)) . alet a be
object ;
( a in M implies (G9 * F9) . a = (def_func' (H,v)) . a )assume
a in M
;
(G9 * F9) . a = (def_func' (H,v)) . athen reconsider m1 =
a as
Element of
M ;
set m3 =
(def_func' (H,v)) . m1;
A67:
(G9 * F9) . m1 = G9 . (F9 . m1)
by FUNCT_2:15;
M,
(v / ((x. 3),m1)) / (
(x. 4),
((def_func' (H,v)) . m1))
|= H
by A30, A66, Th10;
then consider n being
Element of
M such that A68:
M,
((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / (
(x. k),
n)
|= (H3 / ((x. 4),(x. k))) '&' (H2 / ((x. 3),(x. k)))
by ZF_LANG1:73;
A69:
now for x being Variable st x in Free H3 holds
((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . xlet x be
Variable;
( x in Free H3 implies ((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x )assume A70:
x in Free H3
;
((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . xA71:
((v / ((x. 3),m1)) / ((x. 4),n)) . (x. 4) = n
by FUNCT_7:128;
A72:
((v3 / ((x. 3),m1)) / ((x. 4),n)) . (x. 3) = (v3 / ((x. 3),m1)) . (x. 3)
by FUNCT_7:32, ZF_LANG1:76;
A73:
((v / ((x. 3),m1)) / ((x. 4),n)) . (x. 3) = (v / ((x. 3),m1)) . (x. 3)
by FUNCT_7:32, ZF_LANG1:76;
A74:
(v / ((x. 3),m1)) . (x. 3) = m1
by FUNCT_7:128;
(
x = x. 3 or
x = x. 4 or (
x <> x. 3 &
x <> x. 4 ) )
;
then
(
((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x or (
(v / ((x. 3),m1)) . x = v . x &
(v3 / ((x. 3),m1)) . x = v3 . x &
((v / ((x. 3),m1)) / ((x. 4),n)) . x = (v / ((x. 3),m1)) . x &
((v3 / ((x. 3),m1)) / ((x. 4),n)) . x = (v3 / ((x. 3),m1)) . x ) )
by A71, A74, A73, A72, FUNCT_7:32, FUNCT_7:128;
hence
((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x
by A16, A70;
verum end; A75:
now for x being Variable st x in Free H2 holds
((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = ((v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . xlet x be
Variable;
( x in Free H2 implies ((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = ((v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x )assume
x in Free H2
;
((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = ((v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . xthen
( ( not
x in Free H3 &
x <> x. 3 &
x <> x. 4 ) or
x = x. 3 or
x = x. 4 )
by A35;
then
( (
((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = (v / ((x. 3),n)) . x &
(v / ((x. 3),n)) . x = v . x &
v . x = v2 . x &
v2 . x = (v2 / ((x. 3),n)) . x &
(v2 / ((x. 3),n)) . x = ((v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x ) or (
((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = (v / ((x. 3),n)) . x &
(v / ((x. 3),n)) . x = n &
((v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = (v2 / ((x. 3),n)) . x &
(v2 / ((x. 3),n)) . x = n ) or (
((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = (def_func' (H,v)) . m1 &
((v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = (def_func' (H,v)) . m1 ) )
by A16, Lm3, FUNCT_7:32, FUNCT_7:128;
hence
((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = ((v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x
;
verum end; A76:
(((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n)) . (x. k) = n
by FUNCT_7:128;
M,
((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / (
(x. k),
n)
|= H2 / (
(x. 3),
(x. k))
by A68, ZF_MODEL:15;
then
M,
(((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n)) / (
(x. 3),
n)
|= H2
by A34, A76, Th12;
then
M,
((v / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n)) / (
(x. 3),
n)
|= H2
by Th8;
then
M,
((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) / (
(x. k),
n)
|= H2
by A41, A32, Lm3, Th6;
then
M,
(v / ((x. 3),n)) / (
(x. 4),
((def_func' (H,v)) . m1))
|= H2
by A34, Th5;
then
M,
(v2 / ((x. 3),n)) / (
(x. 4),
((def_func' (H,v)) . m1))
|= H2
by A75, ZF_LANG1:75;
then A77:
G9 . n = (def_func' (H,v)) . m1
by A5, A6, A43, Th10;
M,
((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / (
(x. k),
n)
|= H3 / (
(x. 4),
(x. k))
by A68, ZF_MODEL:15;
then
M,
(((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n)) / (
(x. 4),
n)
|= H3
by A42, A76, Th12;
then
M,
((v / ((x. 3),m1)) / ((x. k),n)) / (
(x. 4),
n)
|= H3
by Th8;
then
M,
((v / ((x. 3),m1)) / ((x. 4),n)) / (
(x. k),
n)
|= H3
by A31, FUNCT_7:33, ZF_LANG1:76;
then
M,
(v / ((x. 3),m1)) / (
(x. 4),
n)
|= H3
by A42, Th5;
then
M,
(v3 / ((x. 3),m1)) / (
(x. 4),
n)
|= H3
by A69, ZF_LANG1:75;
hence
(G9 * F9) . a = (def_func' (H,v)) . a
by A3, A11, A12, A13, A77, A67, Th10;
verum end;
hence
G * F = def_func' (H,v)
by FUNCT_2:12; verum