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
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: i <= i3 by A8, XXREAL_0:2;
x. 0 in {(x. 0 ),(x. 1),(x. 2)} by ENUMSET1:def 1;
then A10: ( not x. 0 in Free H1 & not x. 0 in Free H2 ) by A1, A4, XBOOLE_0:3;
then consider H3 being ZF-formula, v3 being Function of VAR ,M such that
A11: for j being Element of NAT st j < i3 & x. j in variables_in H3 & not j = 3 holds
j = 4 and
A12: ( not x. 0 in Free H3 & 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;
A14: {(x. 0 ),(x. 1),(x. 2)} misses Free H3
proof
A15: ( i3 > 0 & i3 > 1 & i3 > 2 ) by A8, XXREAL_0:2;
assume {(x. 0 ),(x. 1),(x. 2)} meets Free H3 ; :: thesis: contradiction
then consider a being set such that
A16: ( a in {(x. 0 ),(x. 1),(x. 2)} & a in Free H3 ) by XBOOLE_0:3;
( ( a = x. 0 or a = x. 1 or a = x. 2 ) & Free H3 c= variables_in H3 ) by A16, ENUMSET1:def 1, ZF_LANG1:164;
hence contradiction by A11, A15, A16; :: thesis: verum
end;
consider k1 being Element of NAT such that
A17: 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
A18: ( ( k1 > i3 & k = k1 ) or ( k1 <= i3 & k = i3 + 1 ) ) ;
A19: 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 A9, A18, NAT_1:13, XXREAL_0:2; :: thesis: verum
end;
A20: not x. k in variables_in H3
proof
assume x. k in variables_in H3 ; :: thesis: contradiction
then k < k1 by A17;
hence contradiction by A18, NAT_1:13; :: thesis: verum
end;
A21: ( k <> 4 & k <> 3 & k <> 0 ) by A8, A18, NAT_1:13, XXREAL_0:2;
then A22: ( x. k <> x. 0 & x. k <> x. 3 & x. k <> x. 4 ) by ZF_LANG1:86;
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 )
defpred S1[ set ] means $1 in Free H3;
deffunc H1( set ) -> set = v3 . $1;
deffunc H2( set ) -> set = v2 . $1;
consider v being Function such that
A23: ( dom v = VAR & ( for a being set st a in VAR holds
( ( S1[a] implies v . a = H1(a) ) & ( not S1[a] implies v . a = H2(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
A24: ( a in dom v & b = v . a ) by FUNCT_1:def 5;
reconsider a = a as Variable by A23, A24;
( b = v3 . a or b = v2 . a ) by A23, A24;
hence b in M ; :: thesis: verum
end;
then reconsider v = v as Function of VAR ,M by A23, 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 )
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 a in (Free ((H3 / (x. 4),(x. k)) '&' (H2 / (x. 3),(x. k)))) \ {(x. k)} by ZF_LANG1:71;
then A27: ( a in Free ((H3 / (x. 4),(x. k)) '&' (H2 / (x. 3),(x. k))) & not a in {(x. k)} & Free ((H3 / (x. 4),(x. k)) '&' (H2 / (x. 3),(x. k))) = (Free (H3 / (x. 4),(x. k))) \/ (Free (H2 / (x. 3),(x. k))) ) by XBOOLE_0:def 5, ZF_LANG1:66;
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 Th1, XBOOLE_0:def 3;
then ( a in (Free H3) \ {(x. 4)} or a in (Free H2) \ {(x. 3)} ) by A27, XBOOLE_0:def 3;
then ( a in Free H3 or a in Free H2 ) by XBOOLE_0:def 5;
hence contradiction by A4, A14, 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 A28: not x. 0 in Free H by A25;
A29: 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 )
A30: ( Free H2 c= variables_in H2 & Free H3 c= variables_in H3 ) by ZF_LANG1:164;
consider j being Element of NAT such that
A31: x = x. j by ZF_LANG1:87;
assume A32: ( x in Free H2 & x in Free H3 ) ; :: thesis: ( x = x. 3 or x = x. 4 )
then j < i3 by A7, A9, A30, A31, XXREAL_0:2;
hence ( x = x. 3 or x = x. 4 ) by A11, A30, A31, A32; :: thesis: verum
end;
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 ) )
consider m being Element of M such that
A33: for m4 being Element of M holds
( M,(v3 / (x. 3),m1) / (x. 4),m4 |= H3 iff m4 = m ) by A12, Th20;
consider r being Element of M such that
A34: for m4 being Element of M holds
( M,(v2 / (x. 3),m) / (x. 4),m4 |= H2 iff m4 = r ) by A5, A10, 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 ) )
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
assume M,(v / (x. 3),m1) / (x. 4),m3 |= H ; :: thesis: m3 = r
then consider n being Element of M such that
A35: 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;
A36: ( M,((v / (x. 3),m1) / (x. 4),m3) / (x. k),n |= H3 / (x. 4),(x. k) & (((v / (x. 3),m1) / (x. 4),m3) / (x. k),n) . (x. k) = n & M,((v / (x. 3),m1) / (x. 4),m3) / (x. k),n |= H2 / (x. 3),(x. k) ) by A35, FUNCT_7:130, ZF_MODEL:15;
then M,(((v / (x. 3),m1) / (x. 4),m3) / (x. k),n) / (x. 4),n |= H3 by A20, 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 A21, FUNCT_7:35, ZF_LANG1:86;
then A37: M,(v / (x. 3),m1) / (x. 4),n |= H3 by A20, Th6;
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 A38: x in Free H3 ; :: thesis: ((v / (x. 3),m1) / (x. 4),n) . x = ((v3 / (x. 3),m1) / (x. 4),n) . x
( ( x = x. 3 or x = x. 4 or ( x <> x. 3 & x <> x. 4 ) ) & ((v / (x. 3),m1) / (x. 4),n) . (x. 4) = n & ((v3 / (x. 3),m1) / (x. 4),n) . (x. 4) = n & (v / (x. 3),m1) . (x. 3) = m1 & (v3 / (x. 3),m1) . (x. 3) = m1 & ((v / (x. 3),m1) / (x. 4),n) . (x. 3) = (v / (x. 3),m1) . (x. 3) & ((v3 / (x. 3),m1) / (x. 4),n) . (x. 3) = (v3 / (x. 3),m1) . (x. 3) ) by Lm1, FUNCT_7:34, FUNCT_7:130;
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 FUNCT_7:34;
hence ((v / (x. 3),m1) / (x. 4),n) . x = ((v3 / (x. 3),m1) / (x. 4),n) . x by A23, A38; :: thesis: verum
end;
then M,(v3 / (x. 3),m1) / (x. 4),n |= H3 by A37, ZF_LANG1:84;
then n = m by A33;
then M,(((v / (x. 3),m1) / (x. 4),m3) / (x. k),m) / (x. 3),m |= H2 by A19, A36, 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 A22, Lm1, Th7;
then A39: M,(v / (x. 3),m) / (x. 4),m3 |= H2 by A19, Th6;
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 A29;
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 A23, Lm1, 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;
then M,(v2 / (x. 3),m) / (x. 4),m3 |= H2 by A39, ZF_LANG1:84;
hence m3 = r by A34; :: thesis: verum
end;
assume m3 = r ; :: thesis: M,(v / (x. 3),m1) / (x. 4),m3 |= H
then ( ((v2 / (x. 3),m) / (x. 4),m3) . (x. 3) = (v2 / (x. 3),m) . (x. 3) & (v2 / (x. 3),m) . (x. 3) = m & M,(v2 / (x. 3),m) / (x. 4),m3 |= H2 ) by A34, Lm1, FUNCT_7:34, FUNCT_7:130;
then M,((v2 / (x. 3),m) / (x. 4),m3) / (x. k),m |= H2 / (x. 3),(x. k) by A19, Th14;
then A40: ( M,((v2 / (x. 4),m3) / (x. k),m) / (x. 3),m |= H2 / (x. 3),(x. k) & not x. 3 in variables_in (H2 / (x. 3),(x. k)) ) by A22, Lm1, Th7, ZF_LANG1:198;
then A41: M,(v2 / (x. 4),m3) / (x. k),m |= H2 / (x. 3),(x. k) by Th6;
( ((v3 / (x. 3),m1) / (x. 4),m) . (x. 4) = m & M,(v3 / (x. 3),m1) / (x. 4),m |= H3 ) by A33, FUNCT_7:130;
then M,((v3 / (x. 3),m1) / (x. 4),m) / (x. k),m |= H3 / (x. 4),(x. k) by A20, Th14;
then A42: ( not x. 4 in variables_in (H3 / (x. 4),(x. k)) & M,((v3 / (x. 3),m1) / (x. k),m) / (x. 4),m |= H3 / (x. 4),(x. k) ) by A22, FUNCT_7:35, ZF_LANG1:198;
then A43: M,(v3 / (x. 3),m1) / (x. k),m |= H3 / (x. 4),(x. k) by Th6;
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 )
A44: Free (H2 / (x. 3),(x. k)) c= ((Free H2) \ {(x. 3)}) \/ {(x. k)} by Th1;
assume 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
then ( x in (Free H2) \ {(x. 3)} or x in {(x. k)} ) by A44, 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 A29, TARSKI:def 1, FUNCT_7:130;
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 A22, A23, 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;
then M,(v / (x. 4),m3) / (x. k),m |= H2 / (x. 3),(x. k) by A41, ZF_LANG1:84;
then M,((v / (x. 4),m3) / (x. k),m) / (x. 3),m1 |= H2 / (x. 3),(x. k) by A40, Th6;
then A45: M,((v / (x. 3),m1) / (x. 4),m3) / (x. k),m |= H2 / (x. 3),(x. k) by A22, Lm1, Th7;
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 )
A46: Free (H3 / (x. 4),(x. k)) c= ((Free H3) \ {(x. 4)}) \/ {(x. k)} by Th1;
assume 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
then ( x in (Free H3) \ {(x. 4)} or x in {(x. k)} ) by A46, 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 TARSKI:def 1, FUNCT_7:130;
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 A22, A23, 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;
then M,(v / (x. 3),m1) / (x. k),m |= H3 / (x. 4),(x. k) by A43, ZF_LANG1:84;
then M,((v / (x. 3),m1) / (x. k),m) / (x. 4),m3 |= H3 / (x. 4),(x. k) by A42, Th6;
then M,((v / (x. 3),m1) / (x. 4),m3) / (x. k),m |= H3 / (x. 4),(x. k) by A21, FUNCT_7:35, ZF_LANG1:86;
then M,((v / (x. 3),m1) / (x. 4),m3) / (x. k),m |= (H3 / (x. 4),(x. k)) '&' (H2 / (x. 3),(x. k)) by A45, ZF_MODEL:15;
hence M,(v / (x. 3),m1) / (x. 4),m3 |= H by ZF_LANG1:82; :: thesis: verum
end;
hence A47: M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) by A28, Th20; :: thesis: G * F = def_func' H,v
reconsider F' = F, G' = G as Function of M,M by A3, A6;
now
let a be set ; :: thesis: ( a in M implies (G' * F') . a = (def_func' H,v) . a )
assume a in M ; :: thesis: (G' * F') . a = (def_func' H,v) . a
then reconsider m1 = a as Element of M ;
set m3 = (def_func' H,v) . m1;
consider n being Element of M;
M,(v / (x. 3),m1) / (x. 4),((def_func' H,v) . m1) |= H by A28, A47, Th11;
then consider n being Element of M such that
A48: 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;
A49: ( M,((v / (x. 3),m1) / (x. 4),((def_func' H,v) . m1)) / (x. k),n |= H3 / (x. 4),(x. k) & (((v / (x. 3),m1) / (x. 4),((def_func' H,v) . m1)) / (x. k),n) . (x. k) = n & M,((v / (x. 3),m1) / (x. 4),((def_func' H,v) . m1)) / (x. k),n |= H2 / (x. 3),(x. k) ) by A48, FUNCT_7:130, ZF_MODEL:15;
then M,(((v / (x. 3),m1) / (x. 4),((def_func' H,v) . m1)) / (x. k),n) / (x. 4),n |= H3 by A20, 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 A21, FUNCT_7:35, ZF_LANG1:86;
then A50: M,(v / (x. 3),m1) / (x. 4),n |= H3 by A20, Th6;
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 A51: x in Free H3 ; :: thesis: ((v / (x. 3),m1) / (x. 4),n) . x = ((v3 / (x. 3),m1) / (x. 4),n) . x
( ( x = x. 3 or x = x. 4 or ( x <> x. 3 & x <> x. 4 ) ) & ((v / (x. 3),m1) / (x. 4),n) . (x. 4) = n & ((v3 / (x. 3),m1) / (x. 4),n) . (x. 4) = n & (v / (x. 3),m1) . (x. 3) = m1 & (v3 / (x. 3),m1) . (x. 3) = m1 & ((v / (x. 3),m1) / (x. 4),n) . (x. 3) = (v / (x. 3),m1) . (x. 3) & ((v3 / (x. 3),m1) / (x. 4),n) . (x. 3) = (v3 / (x. 3),m1) . (x. 3) ) by Lm1, FUNCT_7:34, FUNCT_7:130;
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 FUNCT_7:34;
hence ((v / (x. 3),m1) / (x. 4),n) . x = ((v3 / (x. 3),m1) / (x. 4),n) . x by A23, A51; :: thesis: verum
end;
then A52: M,(v3 / (x. 3),m1) / (x. 4),n |= H3 by A50, ZF_LANG1:84;
M,(((v / (x. 3),m1) / (x. 4),((def_func' H,v) . m1)) / (x. k),n) / (x. 3),n |= H2 by A19, A49, 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 A22, Lm1, Th7;
then A53: M,(v / (x. 3),n) / (x. 4),((def_func' H,v) . m1) |= H2 by A19, Th6;
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 A29;
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 A23, Lm1, 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;
then M,(v2 / (x. 3),n) / (x. 4),((def_func' H,v) . m1) |= H2 by A53, ZF_LANG1:84;
then ( G' . n = (def_func' H,v) . m1 & (G' * F') . m1 = G' . (F' . m1) ) by A5, A6, A10, Th11, FUNCT_2:21;
hence (G' * F') . a = (def_func' H,v) . a by A3, A12, A13, A52, Th11; :: thesis: verum
end;
hence G * F = def_func' H,v by FUNCT_2:18; :: thesis: verum