let M be non empty set ; :: thesis: 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; :: thesis: ( 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) ; :: according to ZFMODEL1:def 4 :: thesis: ( 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) ; :: according to ZFMODEL1:def 4 :: thesis: 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))))); :: according to ZFMODEL1:def 4 :: thesis: 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
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng v or b in M )
assume b in rng v ; :: thesis: b in M
then consider a being object such that
A17: a in dom v and
A18: b = v . a by FUNCT_1:def 3;
reconsider a = a as Variable by A16, A17;
( b = v3 . a or b = v2 . a ) by A16, A18;
hence b in M ; :: thesis: verum
end;
then reconsider v = v as Function of VAR,M by A16, FUNCT_2:def 1, RELSET_1:4;
take v ; :: thesis: ( {(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 ; :: thesis: 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; :: thesis: verum
end;
A25: now :: thesis: for a being object st a in {(x. 0),(x. 1),(x. 2)} holds
not a in Free H
let a be object ; :: thesis: ( a in {(x. 0),(x. 1),(x. 2)} implies not a in Free H )
assume A26: a in {(x. 0),(x. 1),(x. 2)} ; :: thesis: not a in Free H
assume a in Free H ; :: thesis: contradiction
then 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; :: thesis: verum
end;
hence {(x. 0),(x. 1),(x. 2)} misses Free H by XBOOLE_0:3; :: thesis: ( 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
proof
assume x. k in variables_in H2 ; :: thesis: contradiction
then k < i by A7;
hence contradiction by A33, A15, NAT_1:13, XXREAL_0:2; :: thesis: verum
end;
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 )
proof
let x be Variable; :: thesis: ( not x in Free H2 or not x in Free H3 or x = x. 3 or x = x. 4 )
A36: Free H3 c= variables_in H3 by ZF_LANG1:151;
assume that
A37: x in Free H2 and
A38: x in Free H3 ; :: thesis: ( x = x. 3 or x = x. 4 )
consider j being Element of NAT such that
A39: x = x. j by ZF_LANG1:77;
Free H2 c= variables_in H2 by ZF_LANG1:151;
then j < i3 by A7, A33, A39, A37, XXREAL_0:2;
hence ( x = x. 3 or x = x. 4 ) by A10, A36, A39, A38; :: thesis: verum
end;
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
proof
assume x. k in variables_in H3 ; :: thesis: contradiction
then k < k1 by A14;
hence contradiction by A15, NAT_1:13; :: thesis: verum
end;
A43: not x. 0 in Free H2 by A4, A9, XBOOLE_0:3;
now :: thesis: 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; :: thesis: 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 :: thesis: 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)) . x
let x be Variable; :: thesis: ( 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))) ; :: thesis: ((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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ) :: thesis: ( m3 = r implies M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H )
proof
A50: now :: thesis: 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)) . x
let x be Variable; :: thesis: ( 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 ; :: thesis: ((v / ((x. 3),m)) / ((x. 4),m3)) . x = ((v2 / ((x. 3),m)) / ((x. 4),m3)) . x
then ( ( 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 ; :: thesis: verum
end;
assume M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H ; :: thesis: 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 :: thesis: 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)) . x
let x be Variable; :: thesis: ( 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 ; :: thesis: ((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x
A54: ((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; :: thesis: 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; :: thesis: verum
end;
assume m3 = r ; :: thesis: M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H
then 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 :: thesis: 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)) . x
let x be Variable; :: thesis: ( 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))) ; :: thesis: ((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 ; :: thesis: 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; :: thesis: verum
end;
hence A66: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) by A30, Th19; :: thesis: G * F = def_func' (H,v)
now :: thesis: for a being object st a in M holds
(G9 * F9) . a = (def_func' (H,v)) . a
let a be object ; :: thesis: ( a in M implies (G9 * F9) . a = (def_func' (H,v)) . a )
assume a in M ; :: thesis: (G9 * F9) . a = (def_func' (H,v)) . a
then 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 :: thesis: 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)) . x
let x be Variable; :: thesis: ( 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 ; :: thesis: ((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x
A71: ((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; :: thesis: verum
end;
A75: now :: thesis: 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))) . x
let x be Variable; :: thesis: ( 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 ; :: thesis: ((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = ((v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x
then ( ( 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 ; :: thesis: 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; :: thesis: verum
end;
hence G * F = def_func' (H,v) by FUNCT_2:12; :: thesis: verum