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( set ) -> 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 Th4;
( 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, Th17;
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 Th4;
( 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( set ) -> set = v3 . $1;
defpred S1[ set ] 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 K29(K30(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 set 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 set ; :: 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 set such that
A17: a in dom v and
A18: b = v . a by FUNCT_1:def 5;
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:11;
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 set 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:164;
( 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
let a be set ; :: 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:71;
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:66;
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:86;
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:164;
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:87;
Free H2 c= variables_in H2 by ZF_LANG1:164;
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:86;
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
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:86, ZF_LANG1:198;
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, Th20;
A46: now
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:130, 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:34, FUNCT_7:130;
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, Th20;
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:130;
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
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:34, FUNCT_7:130;
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:82;
A52: now
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:130;
A55: ((v3 / (x. 3),m1) / (x. 4),n) . (x. 3) = (v3 / (x. 3),m1) . (x. 3) by FUNCT_7:34, ZF_LANG1:86;
A56: ((v / (x. 3),m1) / (x. 4),n) . (x. 3) = (v / (x. 3),m1) . (x. 3) by FUNCT_7:34, ZF_LANG1:86;
A57: (v / (x. 3),m1) . (x. 3) = m1 by FUNCT_7:130;
( 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:34, FUNCT_7:130;
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:130;
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, Th13;
then M,((v / (x. 3),m1) / (x. k),n) / (x. 4),n |= H3 by Th9;
then M,((v / (x. 3),m1) / (x. 4),n) / (x. k),n |= H3 by A31, FUNCT_7:35, ZF_LANG1:86;
then M,(v / (x. 3),m1) / (x. 4),n |= H3 by A42, Th6;
then M,(v3 / (x. 3),m1) / (x. 4),n |= H3 by A52, ZF_LANG1:84;
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, Th13;
then M,((v / (x. 4),m3) / (x. k),m) / (x. 3),m |= H2 by Th9;
then M,((v / (x. 3),m) / (x. 4),m3) / (x. k),m |= H2 by A41, A32, Lm3, Th7;
then M,(v / (x. 3),m) / (x. 4),m3 |= H2 by A34, Th6;
then M,(v2 / (x. 3),m) / (x. 4),m3 |= H2 by A50, ZF_LANG1:84;
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:130;
A62: now
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:130, 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:34, FUNCT_7:130;
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:86, ZF_LANG1:198;
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, Th14;
then M,((v3 / (x. 3),m1) / (x. k),m) / (x. 4),m |= H3 / (x. 4),(x. k) by A31, FUNCT_7:35, ZF_LANG1:86;
then M,(v3 / (x. 3),m1) / (x. k),m |= H3 / (x. 4),(x. k) by A64, Th6;
then M,(v / (x. 3),m1) / (x. k),m |= H3 / (x. 4),(x. k) by A46, ZF_LANG1:84;
then M,((v / (x. 3),m1) / (x. k),m) / (x. 4),m3 |= H3 / (x. 4),(x. k) by A64, Th6;
then A65: M,((v / (x. 3),m1) / (x. 4),m3) / (x. k),m |= H3 / (x. 4),(x. k) by A31, FUNCT_7:35, ZF_LANG1:86;
((v2 / (x. 3),m) / (x. 4),m3) . (x. 3) = (v2 / (x. 3),m) . (x. 3) by FUNCT_7:34, ZF_LANG1:86;
then M,((v2 / (x. 3),m) / (x. 4),m3) / (x. k),m |= H2 / (x. 3),(x. k) by A34, A61, A60, Th14;
then M,((v2 / (x. 4),m3) / (x. k),m) / (x. 3),m |= H2 / (x. 3),(x. k) by A41, A32, Lm3, Th7;
then M,(v2 / (x. 4),m3) / (x. k),m |= H2 / (x. 3),(x. k) by A44, Th6;
then M,(v / (x. 4),m3) / (x. k),m |= H2 / (x. 3),(x. k) by A62, ZF_LANG1:84;
then M,((v / (x. 4),m3) / (x. k),m) / (x. 3),m1 |= H2 / (x. 3),(x. k) by A44, Th6;
then M,((v / (x. 3),m1) / (x. 4),m3) / (x. k),m |= H2 / (x. 3),(x. k) by A41, A32, Lm3, Th7;
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:82; :: thesis: verum
end;
hence A66: M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) by A30, Th20; :: thesis: G * F = def_func' H,v
now
consider n being Element of M;
let a be set ; :: 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:21;
M,(v / (x. 3),m1) / (x. 4),((def_func' H,v) . m1) |= H by A30, A66, Th11;
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:82;
A69: now
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:130;
A72: ((v3 / (x. 3),m1) / (x. 4),n) . (x. 3) = (v3 / (x. 3),m1) . (x. 3) by FUNCT_7:34, ZF_LANG1:86;
A73: ((v / (x. 3),m1) / (x. 4),n) . (x. 3) = (v / (x. 3),m1) . (x. 3) by FUNCT_7:34, ZF_LANG1:86;
A74: (v / (x. 3),m1) . (x. 3) = m1 by FUNCT_7:130;
( 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:34, FUNCT_7:130;
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
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:34, FUNCT_7:130;
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:130;
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, Th13;
then M,((v / (x. 4),((def_func' H,v) . m1)) / (x. k),n) / (x. 3),n |= H2 by Th9;
then M,((v / (x. 3),n) / (x. 4),((def_func' H,v) . m1)) / (x. k),n |= H2 by A41, A32, Lm3, Th7;
then M,(v / (x. 3),n) / (x. 4),((def_func' H,v) . m1) |= H2 by A34, Th6;
then M,(v2 / (x. 3),n) / (x. 4),((def_func' H,v) . m1) |= H2 by A75, ZF_LANG1:84;
then A77: G9 . n = (def_func' H,v) . m1 by A5, A6, A43, Th11;
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, Th13;
then M,((v / (x. 3),m1) / (x. k),n) / (x. 4),n |= H3 by Th9;
then M,((v / (x. 3),m1) / (x. 4),n) / (x. k),n |= H3 by A31, FUNCT_7:35, ZF_LANG1:86;
then M,(v / (x. 3),m1) / (x. 4),n |= H3 by A42, Th6;
then M,(v3 / (x. 3),m1) / (x. 4),n |= H3 by A69, ZF_LANG1:84;
hence (G9 * F9) . a = (def_func' H,v) . a by A3, A11, A12, A13, A77, A67, Th11; :: thesis: verum
end;
hence G * F = def_func' H,v by FUNCT_2:18; :: thesis: verum