let n be natural non empty number ; :: thesis: 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 S being non empty non void b₁ -extension n PC-correct QC-correct QCLangSignature over Union X
for Y being empty-yielding b₃ -tolerating ManySortedSet of the carrier of S
for L being non-empty Language of Y,S st L is subst-correct & Y is ManySortedSubset of the Sorts of L holds
for x, y being Element of Union Y
for a being SortSymbol of S st x in Y . a & y in Y . a holds
for A being Formula of L holds
( (\not A) / (x,y) = \not (A / (x,y)) & ( for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L ) ) )
let J be non empty non void Signature; :: thesis: for T being non-empty MSAlgebra over J
for X being empty-yielding GeneratorSet of T
for S being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X
for Y being empty-yielding b₂ -tolerating ManySortedSet of the carrier of S
for L being non-empty Language of Y,S st L is subst-correct & Y is ManySortedSubset of the Sorts of L holds
for x, y being Element of Union Y
for a being SortSymbol of S st x in Y . a & y in Y . a holds
for A being Formula of L holds
( (\not A) / (x,y) = \not (A / (x,y)) & ( for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L ) ) )
let T be non-empty MSAlgebra over J; :: thesis: for X being empty-yielding GeneratorSet of T
for S being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X
for Y being empty-yielding b₁ -tolerating ManySortedSet of the carrier of S
for L being non-empty Language of Y,S st L is subst-correct & Y is ManySortedSubset of the Sorts of L holds
for x, y being Element of Union Y
for a being SortSymbol of S st x in Y . a & y in Y . a holds
for A being Formula of L holds
( (\not A) / (x,y) = \not (A / (x,y)) & ( for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L ) ) )
let X be empty-yielding GeneratorSet of T; :: thesis: for S being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X
for Y being empty-yielding X -tolerating ManySortedSet of the carrier of S
for L being non-empty Language of Y,S st L is subst-correct & Y is ManySortedSubset of the Sorts of L holds
for x, y being Element of Union Y
for a being SortSymbol of S st x in Y . a & y in Y . a holds
for A being Formula of L holds
( (\not A) / (x,y) = \not (A / (x,y)) & ( for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L ) ) )
let S be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X; :: thesis: for Y being empty-yielding X -tolerating ManySortedSet of the carrier of S
for L being non-empty Language of Y,S st L is subst-correct & Y is ManySortedSubset of the Sorts of L holds
for x, y being Element of Union Y
for a being SortSymbol of S st x in Y . a & y in Y . a holds
for A being Formula of L holds
( (\not A) / (x,y) = \not (A / (x,y)) & ( for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L ) ) )
let Y be empty-yielding X -tolerating ManySortedSet of the carrier of S; :: thesis: for L being non-empty Language of Y,S st L is subst-correct & Y is ManySortedSubset of the Sorts of L holds
for x, y being Element of Union Y
for a being SortSymbol of S st x in Y . a & y in Y . a holds
for A being Formula of L holds
( (\not A) / (x,y) = \not (A / (x,y)) & ( for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L ) ) )
let L be non-empty Language of Y,S; :: thesis: ( L is subst-correct & Y is ManySortedSubset of the Sorts of L implies for x, y being Element of Union Y
for a being SortSymbol of S st x in Y . a & y in Y . a holds
for A being Formula of L holds
( (\not A) / (x,y) = \not (A / (x,y)) & ( for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L ) ) ) )
assume that
A1: L is subst-correct and
A2: Y is ManySortedSubset of the Sorts of L ; :: thesis: for x, y being Element of Union Y
for a being SortSymbol of S st x in Y . a & y in Y . a holds
for A being Formula of L holds
( (\not A) / (x,y) = \not (A / (x,y)) & ( for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L ) ) )
let x, y be Element of Union Y; :: thesis: for a being SortSymbol of S st x in Y . a & y in Y . a holds
for A being Formula of L holds
( (\not A) / (x,y) = \not (A / (x,y)) & ( for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L ) ) )
let a be SortSymbol of S; :: thesis: ( x in Y . a & y in Y . a implies for A being Formula of L holds
( (\not A) / (x,y) = \not (A / (x,y)) & ( for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L ) ) ) )
assume A3: ( x in Y . a & y in Y . a ) ; :: thesis: for A being Formula of L holds
( (\not A) / (x,y) = \not (A / (x,y)) & ( for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L ) ) )
Y c= the Sorts of L by A2, PBOOLE:def 18;
then Y . a c= the Sorts of L . a ;
then reconsider t = y as Element of the Sorts of L . a by A3;
let A be Formula of L; :: thesis: ( (\not A) / (x,y) = \not (A / (x,y)) & ( for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L ) ) )
reconsider aa = <*A*> as Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) by Th25;
set f = the formula-sort of S;

B1: now :: thesis: for i being natural number st i in dom the connectives of S holds
for S1 being QCLangSignature over Union Y st S = S1 holds
for z being Element of Union Y
for q being Element of {1,2} holds In (( the connectives of S . i), the carrier' of S) <> the quantifiers of S1 . (q,z)

let i be natural number ; :: thesis: ( i in dom the connectives of S implies for S1 being QCLangSignature over Union Y st S = S1 holds
for z being Element of Union Y
for q being Element of {1,2} holds In (( the connectives of S . i), the carrier' of S) <> the quantifiers of S1 . (q,z) )
assume i in dom the connectives of S ; :: thesis: for S1 being QCLangSignature over Union Y st S = S1 holds
for z being Element of Union Y
for q being Element of {1,2} holds In (( the connectives of S . i), the carrier' of S) <> the quantifiers of S1 . (q,z)
then ( the connectives of S . i in rng the connectives of S & rng the connectives of S c= the carrier' of S ) by FUNCT_1:def 3;
then B7: In (( the connectives of S . i), the carrier' of S) in rng the connectives of S by SUBSET_1:def 8;
let S1 be QCLangSignature over Union Y; :: thesis: ( S = S1 implies for z being Element of Union Y
for q being Element of {1,2} holds In (( the connectives of S . i), the carrier' of S) <> the quantifiers of S1 . (q,z) )
assume B5: S = S1 ; :: thesis: for z being Element of Union Y
for q being Element of {1,2} holds In (( the connectives of S . i), the carrier' of S) <> the quantifiers of S1 . (q,z)
let z be Element of Union Y; :: thesis: for q being Element of {1,2} holds In (( the connectives of S . i), the carrier' of S) <> the quantifiers of S1 . (q,z)
let q be Element of {1,2}; :: thesis: In (( the connectives of S . i), the carrier' of S) <> the quantifiers of S1 . (q,z)
( [q,z] in [:{1,2},(Union Y):] & the quant-sort of S = {1,2} ) by Def5, ZFMISC_1:87;
then ( the quantifiers of S1 . [q,z] in rng the quantifiers of S & rng the quantifiers of S misses rng the connectives of S ) by B5, Def5, FUNCT_2:4;
hence In (( the connectives of S . i), the carrier' of S) <> the quantifiers of S1 . (q,z) by B7, XBOOLE_0:3; :: thesis: verum

end;

A4: len the connectives of S >= n + 5 by Def4;
( 0 < n & n <= n + 5 ) by NAT_1:11;
then ( 0 + 1 <= n & n <= len the connectives of S ) by A4, NAT_1:13, XXREAL_0:2;
then B2: n in dom the connectives of S by FINSEQ_3:25;
then ( the connectives of S . n = In (( the connectives of S . n), the carrier' of S) & the connectives of S . n is_of_type <* the formula-sort of S*>, the formula-sort of S ) by SUBSET_1:def 8, Def4, FUNCT_1:102;
then A5: ( aa / (x,t) = <*(A / (x,t))*> & the_result_sort_of (In (( the connectives of S . n), the carrier' of S)) = the formula-sort of S ) by A3, Th26;
B3: for S1 being QCLangSignature over Union Y holds
( not S = S1 or for z being Element of Union Y
for q being Element of {1,2} holds not In (( the connectives of S . n), the carrier' of S) = the quantifiers of S1 . (q,z) ) by B1, B2;
thus (\not A) / (x,y) = (\not A) / (x,t) by A3, A2, Th14
.= \not (A / (x,t)) by A5, A1, A3, B3
.= \not (A / (x,y)) by A3, A2, Th14 ; :: thesis: for B being Formula of L holds
( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L )
let B be Formula of L; :: thesis: ( (A \and B) / (x,y) = (A / (x,y)) \and (B / (x,y)) & (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L )
A6: <*A,B*> in Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),L) & ... & <*A,B*> in Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),L) by Th25;
A7: for a being Element of Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),L) st <*A,B*> = a holds
a / (x,t) = <*(A / (x,t)),(B / (x,t))*> & ... & for a being Element of Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),L) st <*A,B*> = a holds
a / (x,t) = <*(A / (x,t)),(B / (x,t))*> by A3, Th26;
reconsider a1 = <*A,B*> as Element of Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),L) by A6;
reconsider a2 = <*A,B*> as Element of Args ((In (( the connectives of S . (n + 2)), the carrier' of S)),L) by A6;
reconsider a3 = <*A,B*> as Element of Args ((In (( the connectives of S . (n + 3)), the carrier' of S)),L) by A6;
reconsider a4 = <*A,B*> as Element of Args ((In (( the connectives of S . (n + 4)), the carrier' of S)),L) by A6;
( 1 <= n + 1 & n + 1 <= (n + 1) + 4 ) by NAT_1:11;
then ( 1 <= n + 1 & n + 1 <= len the connectives of S ) by A4, XXREAL_0:2;
then B4: n + 1 in dom the connectives of S by FINSEQ_3:25;
then A8: ( the connectives of S . (n + 1) = In (( the connectives of S . (n + 1)), the carrier' of S) & the connectives of S . (n + 1) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S & ... & the connectives of S . (n + 4) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S ) by Def4, SUBSET_1:def 8, FUNCT_1:102;
then In (( the connectives of S . (n + 1)), the carrier' of S) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S ;
then A9: ( a1 / (x,t) = <*(A / (x,t)),(B / (x,t))*> & the_result_sort_of (In (( the connectives of S . (n + 1)), the carrier' of S)) = the formula-sort of S ) by A7;
B3: for S1 being QCLangSignature over Union Y holds
( not S = S1 or for z being Element of Union Y
for q being Element of {1,2} holds not In (( the connectives of S . (n + 1)), the carrier' of S) = the quantifiers of S1 . (q,z) ) by B1, B4;
thus (A \and B) / (x,y) = (A \and B) / (x,t) by A3, A2, Th14
.= (A / (x,t)) \and (B / (x,t)) by A1, A3, A9, B3
.= (A / (x,y)) \and (B / (x,t)) by A3, A2, Th14
.= (A / (x,y)) \and (B / (x,y)) by A3, A2, Th14 ; :: thesis: ( (A \or B) / (x,y) = (A / (x,y)) \or (B / (x,y)) & (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L )
( 1 + 1 <= n + 2 & n + 2 <= (n + 2) + 3 ) by NAT_1:11;
then ( 1 <= n + 2 & n + 2 <= len the connectives of S ) by A4, XXREAL_0:2;
then B4: n + 2 in dom the connectives of S by FINSEQ_3:25;
then ( the connectives of S . (n + 2) = In (( the connectives of S . (n + 2)), the carrier' of S) & the connectives of S . (n + 2) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S ) by A8, SUBSET_1:def 8, FUNCT_1:102;
then A10: ( a2 / (x,t) = <*(A / (x,t)),(B / (x,t))*> & the_result_sort_of (In (( the connectives of S . (n + 2)), the carrier' of S)) = the formula-sort of S ) by A7;
B3: for S1 being QCLangSignature over Union Y holds
( not S = S1 or for z being Element of Union Y
for q being Element of {1,2} holds not In (( the connectives of S . (n + 2)), the carrier' of S) = the quantifiers of S1 . (q,z) ) by B1, B4;
thus (A \or B) / (x,y) = (A \or B) / (x,t) by A3, A2, Th14
.= (A / (x,t)) \or (B / (x,t)) by A1, A3, A10, B3
.= (A / (x,y)) \or (B / (x,t)) by A3, A2, Th14
.= (A / (x,y)) \or (B / (x,y)) by A3, A2, Th14 ; :: thesis: ( (A \imp B) / (x,y) = (A / (x,y)) \imp (B / (x,y)) & (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L )
( 1 <= (n + 2) + 1 & (n + 2) + 1 <= (n + 3) + 2 ) by NAT_1:11;
then ( 1 <= n + 3 & n + 3 <= len the connectives of S ) by A4, XXREAL_0:2;
then B4: n + 3 in dom the connectives of S by FINSEQ_3:25;
then ( the connectives of S . (n + 3) = In (( the connectives of S . (n + 3)), the carrier' of S) & the connectives of S . (n + 3) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S ) by A8, SUBSET_1:def 8, FUNCT_1:102;
then A11: ( a3 / (x,t) = <*(A / (x,t)),(B / (x,t))*> & the_result_sort_of (In (( the connectives of S . (n + 3)), the carrier' of S)) = the formula-sort of S ) by A7;
B3: for S1 being QCLangSignature over Union Y holds
( not S = S1 or for z being Element of Union Y
for q being Element of {1,2} holds not In (( the connectives of S . (n + 3)), the carrier' of S) = the quantifiers of S1 . (q,z) ) by B1, B4;
thus (A \imp B) / (x,y) = (A \imp B) / (x,t) by A3, A2, Th14
.= (A / (x,t)) \imp (B / (x,t)) by A1, A3, A11, B3
.= (A / (x,y)) \imp (B / (x,t)) by A3, A2, Th14
.= (A / (x,y)) \imp (B / (x,y)) by A3, A2, Th14 ; :: thesis: ( (A \iff B) / (x,y) = (A / (x,y)) \iff (B / (x,y)) & (\true_ L) / (x,y) = \true_ L )
( 1 <= (n + 3) + 1 & (n + 3) + 1 <= (n + 4) + 1 ) by NAT_1:11;
then ( 1 <= n + 4 & n + 4 <= len the connectives of S ) by A4, XXREAL_0:2;
then B4: n + 4 in dom the connectives of S by FINSEQ_3:25;
then ( the connectives of S . (n + 4) = In (( the connectives of S . (n + 4)), the carrier' of S) & the connectives of S . (n + 4) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S ) by A8, SUBSET_1:def 8, FUNCT_1:102;
then A12: ( a4 / (x,t) = <*(A / (x,t)),(B / (x,t))*> & the_result_sort_of (In (( the connectives of S . (n + 4)), the carrier' of S)) = the formula-sort of S ) by A7;
B3: for S1 being QCLangSignature over Union Y holds
( not S = S1 or for z being Element of Union Y
for q being Element of {1,2} holds not In (( the connectives of S . (n + 4)), the carrier' of S) = the quantifiers of S1 . (q,z) ) by B1, B4;
thus (A \iff B) / (x,y) = (A \iff B) / (x,t) by A3, A2, Th14
.= (A / (x,t)) \iff (B / (x,t)) by A1, A3, A12, B3
.= (A / (x,y)) \iff (B / (x,t)) by A3, A2, Th14
.= (A / (x,y)) \iff (B / (x,y)) by A3, A2, Th14 ; :: thesis: (\true_ L) / (x,y) = \true_ L
reconsider ab = {} as Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) by Th25;
( 1 <= (n + 4) + 1 & (n + 4) + 1 <= n + 5 ) by NAT_1:11;
then B4: n + 5 in dom the connectives of S by A4, FINSEQ_3:25;
then ( the connectives of S . (n + 5) = In (( the connectives of S . (n + 5)), the carrier' of S) & the connectives of S . (n + 5) is_of_type {} , the formula-sort of S ) by Def4, SUBSET_1:def 8, FUNCT_1:102;
then A13: ( ab / (x,t) = ab & the_result_sort_of (In (( the connectives of S . (n + 5)), the carrier' of S)) = the formula-sort of S ) by A3, Th26;
B3: for S1 being QCLangSignature over Union Y holds
( not S = S1 or for z being Element of Union Y
for q being Element of {1,2} holds not In (( the connectives of S . (n + 5)), the carrier' of S) = the quantifiers of S1 . (q,z) ) by B1, B4;
thus (\true_ L) / (x,y) = (\true_ L) / (x,t) by A3, A2, Th14
.= \true_ L by A1, A3, A13, B3 ; :: thesis: verum