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 V3() GeneratorSet of T

for S being non empty non void b_{1} -extension n PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{3} -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 V3() GeneratorSet of T

for S being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{2} -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 V3() GeneratorSet of T

for S being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b_{1} -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 V3() 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 V3() 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 V3() 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 V3() 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;

( 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

for T being non-empty MSAlgebra over J

for X being V3() GeneratorSet of T

for S being non empty non void b

for Y being V3() b

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 V3() GeneratorSet of T

for S being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b

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 V3() GeneratorSet of T

for S being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X

for Y being V3() b

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 V3() 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 V3() 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 V3() 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 V3() 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)

A4:
len the connectives of S >= n + 5
by Def4;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;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

( 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