let n be non empty Nat; for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being empty-yielding GeneratorSet of T
for S1 being non empty non void b1 -extension n PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x, y being Element of Union X
for x0, y0 being Element of Union (X extended_by ({}, the carrier of S1)) st L is subst-correct holds
for a being SortSymbol of J st x in X . a & y in X . a & x0 = x & y0 = y holds
(A / (x0,y0)) \imp (\ex (x,A)) in G
let J be non empty non void Signature; for T being non-empty MSAlgebra over J
for X being empty-yielding GeneratorSet of T
for S1 being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x, y being Element of Union X
for x0, y0 being Element of Union (X extended_by ({}, the carrier of S1)) st L is subst-correct holds
for a being SortSymbol of J st x in X . a & y in X . a & x0 = x & y0 = y holds
(A / (x0,y0)) \imp (\ex (x,A)) in G
let T be non-empty MSAlgebra over J; for X being empty-yielding GeneratorSet of T
for S1 being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x, y being Element of Union X
for x0, y0 being Element of Union (X extended_by ({}, the carrier of S1)) st L is subst-correct holds
for a being SortSymbol of J st x in X . a & y in X . a & x0 = x & y0 = y holds
(A / (x0,y0)) \imp (\ex (x,A)) in G
let X be empty-yielding GeneratorSet of T; for S1 being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x, y being Element of Union X
for x0, y0 being Element of Union (X extended_by ({}, the carrier of S1)) st L is subst-correct holds
for a being SortSymbol of J st x in X . a & y in X . a & x0 = x & y0 = y holds
(A / (x0,y0)) \imp (\ex (x,A)) in G
let S1 be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X; for L being non-empty Language of X extended_by ({}, the carrier of S1),S1
for G being QC-theory of L
for A being Formula of L
for x, y being Element of Union X
for x0, y0 being Element of Union (X extended_by ({}, the carrier of S1)) st L is subst-correct holds
for a being SortSymbol of J st x in X . a & y in X . a & x0 = x & y0 = y holds
(A / (x0,y0)) \imp (\ex (x,A)) in G
let L be non-empty Language of X extended_by ({}, the carrier of S1),S1; for G being QC-theory of L
for A being Formula of L
for x, y being Element of Union X
for x0, y0 being Element of Union (X extended_by ({}, the carrier of S1)) st L is subst-correct holds
for a being SortSymbol of J st x in X . a & y in X . a & x0 = x & y0 = y holds
(A / (x0,y0)) \imp (\ex (x,A)) in G
let G be QC-theory of L; for A being Formula of L
for x, y being Element of Union X
for x0, y0 being Element of Union (X extended_by ({}, the carrier of S1)) st L is subst-correct holds
for a being SortSymbol of J st x in X . a & y in X . a & x0 = x & y0 = y holds
(A / (x0,y0)) \imp (\ex (x,A)) in G
let A be Formula of L; for x, y being Element of Union X
for x0, y0 being Element of Union (X extended_by ({}, the carrier of S1)) st L is subst-correct holds
for a being SortSymbol of J st x in X . a & y in X . a & x0 = x & y0 = y holds
(A / (x0,y0)) \imp (\ex (x,A)) in G
let x, y be Element of Union X; for x0, y0 being Element of Union (X extended_by ({}, the carrier of S1)) st L is subst-correct holds
for a being SortSymbol of J st x in X . a & y in X . a & x0 = x & y0 = y holds
(A / (x0,y0)) \imp (\ex (x,A)) in G
let x0, y0 be Element of Union (X extended_by ({}, the carrier of S1)); ( L is subst-correct implies for a being SortSymbol of J st x in X . a & y in X . a & x0 = x & y0 = y holds
(A / (x0,y0)) \imp (\ex (x,A)) in G )
set Y = X extended_by ({}, the carrier of S1);
assume A1:
L is subst-correct
; for a being SortSymbol of J st x in X . a & y in X . a & x0 = x & y0 = y holds
(A / (x0,y0)) \imp (\ex (x,A)) in G
let a be SortSymbol of J; ( x in X . a & y in X . a & x0 = x & y0 = y implies (A / (x0,y0)) \imp (\ex (x,A)) in G )
assume A2:
( x in X . a & y in X . a & x0 = x & y0 = y )
; (A / (x0,y0)) \imp (\ex (x,A)) in G
J is Subsignature of S1
by Def2;
then
the carrier of J c= the carrier of S1
by INSTALG1:10;
then A3:
( a in the carrier of S1 & X c= the Sorts of T & dom the Sorts of L = the carrier of S1 )
by PARTFUN1:def 2, PBOOLE:def 18;
then
( the Sorts of L . a in rng the Sorts of L & the Sorts of L . a = the Sorts of T . a )
by Th16, FUNCT_1:def 3;
then A4:
( X . a c= the Sorts of T . a & the Sorts of T . a = the Sorts of L . a & the Sorts of L . a c= Union the Sorts of L )
by A3, ZFMISC_1:74;
then reconsider t = y as Element of Union the Sorts of L by A2;
A5:
a is SortSymbol of S1
by Th8;
then A6:
( x in (X extended_by ({}, the carrier of S1)) . a & y in (X extended_by ({}, the carrier of S1)) . a )
by A2, Th2;
A7:
X extended_by ({}, the carrier of S1) is ManySortedSubset of the Sorts of L
by Th23;
(\for (x,(\not A))) \imp ((\not A) / (x0,t)) in G
by A2, A4, A6, Def39;
then
(\for (x,(\not A))) \imp ((\not A) / (x0,y0)) in G
by A2, A6, A7, A5, Th14;
then
(\not ((\not A) / (x0,y0))) \imp (\not (\for (x,(\not A)))) in G
by Th58;
then
( (\not (\not (A / (x0,y0)))) \imp (\not (\for (x,(\not A)))) in G & (A / (x0,y0)) \imp (\not (\not (A / (x0,y0)))) in G & (\ex (x,A)) \iff (\not (\for (x,(\not A)))) in G & ((\ex (x,A)) \iff (\not (\for (x,(\not A))))) \imp ((\not (\for (x,(\not A)))) \imp (\ex (x,A))) in G )
by A1, A2, A6, A7, A5, Th27, Def38, Th64, Th105;
then
( (A / (x0,y0)) \imp (\not (\for (x,(\not A)))) in G & (\not (\for (x,(\not A)))) \imp (\ex (x,A)) in G )
by Th45, Def38;
hence
(A / (x0,y0)) \imp (\ex (x,A)) in G
by Th45; verum