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

for x being Element of Union Y

for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

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

for x being Element of Union Y

for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

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

for x being Element of Union Y

for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

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

for x being Element of Union Y

for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

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

for x being Element of Union Y

for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

let Y be V3() X -tolerating ManySortedSet of the carrier of S; :: thesis: for L being non-empty Language of Y,S

for x being Element of Union Y

for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

let L be non-empty Language of Y,S; :: thesis: for x being Element of Union Y

for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

let x be Element of Union Y; :: thesis: for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

let t be Element of Union the Sorts of L; :: thesis: for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

let s be SortSymbol of S; :: thesis: ( x in Y . s & t in the Sorts of L . s implies ( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) ) )

set f = the formula-sort of S;

assume ( x in Y . s & t in the Sorts of L . s ) ; :: thesis: ( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

A1: len the connectives of S >= n + 5 by Def4;

n > 0 ;

then A2: n >= 0 + 1 by NAT_1:13;

n + 0 <= n + 5 & ... & n + 4 <= n + 5 by XREAL_1:6;

then ( 1 <= n + 0 & ... & 1 <= n + 5 & n + 0 <= len the connectives of S & ... & n + 5 <= len the connectives of S ) by A1, A2, NAT_1:12, XXREAL_0:2;

then A3: n + 0 in dom the connectives of S & ... & n + 5 in dom the connectives of S by FINSEQ_3:25;

A4: ( the connectives of S . (n + 0) is_of_type <* the formula-sort of S*>, the formula-sort 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 & the connectives of S . (n + 5) is_of_type {} , the formula-sort of S ) by Def4;

A5: ( In (( the connectives of S . n), the carrier' of S) is_of_type <* the formula-sort of S*>, the formula-sort of S & 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 & ... & In (( the connectives of S . (n + 4)), the carrier' of S) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S & In (( the connectives of S . (n + 5)), the carrier' of S) is_of_type {} , the formula-sort of S ) by A4, A3, FUNCT_1:102, SUBSET_1:def 8;

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) )

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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) )

thus 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))*> :: thesis: for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) )

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) )

let a be Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L); :: thesis: ( <*A*> = a implies a / (x,t) = <*(A / (x,t))*> )

assume a = <*A*> ; :: thesis: a / (x,t) = <*(A / (x,t))*>

then A15: ( Seg 1 = dom a & a . 1 = A & len a = 1 & dom a = dom (the_arity_of (In (( the quantifiers of S . (2,z)), the carrier' of S))) & dom (the_arity_of (In (( the quantifiers of S . (2,z)), the carrier' of S))) = dom (a / (x,t)) ) by MSUALG_6:2, FINSEQ_1:40, FINSEQ_1:89;

consider j being SortSymbol of S such that

A16: ( j = (the_arity_of (In (( the quantifiers of S . (2,z)), the carrier' of S))) . 1 & ex A being Element of L,j st

( A = a . 1 & (a / (x,t)) . 1 = A / (x,t) ) ) by A15, Def14, FINSEQ_1:1;

A17: ( 2 in {1,2} & the quant-sort of S = {1,2} & z in Union X ) by Def5, TARSKI:def 2;

then [2,z] in [: the quant-sort of S,(Union X):] by ZFMISC_1:87;

then In (( the quantifiers of S . (2,z)), the carrier' of S) = the quantifiers of S . (2,z) by SUBSET_1:def 8, FUNCT_2:5;

then In (( the quantifiers of S . (2,z)), the carrier' of S) is_of_type <* the formula-sort of S*>, the formula-sort of S by A17, Def5;

then ( j = the formula-sort of S & len (a / (x,t)) = 1 ) by A15, A16, FINSEQ_1:40, FINSEQ_3:29;

hence a / (x,t) = <*(A / (x,t))*> by A16, A15, FINSEQ_1:40; :: 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

for x being Element of Union Y

for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

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

for x being Element of Union Y

for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

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

for x being Element of Union Y

for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

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

for x being Element of Union Y

for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

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

for x being Element of Union Y

for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

let Y be V3() X -tolerating ManySortedSet of the carrier of S; :: thesis: for L being non-empty Language of Y,S

for x being Element of Union Y

for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

let L be non-empty Language of Y,S; :: thesis: for x being Element of Union Y

for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

let x be Element of Union Y; :: thesis: for t being Element of Union the Sorts of L

for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

let t be Element of Union the Sorts of L; :: thesis: for s being SortSymbol of S st x in Y . s & t in the Sorts of L . s holds

( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

let s be SortSymbol of S; :: thesis: ( x in Y . s & t in the Sorts of L . s implies ( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) ) )

set f = the formula-sort of S;

assume ( x in Y . s & t in the Sorts of L . s ) ; :: thesis: ( ( for a being Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L) st a = {} holds

a / (x,t) = {} ) & ( for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) ) ) )

A1: len the connectives of S >= n + 5 by Def4;

n > 0 ;

then A2: n >= 0 + 1 by NAT_1:13;

n + 0 <= n + 5 & ... & n + 4 <= n + 5 by XREAL_1:6;

then ( 1 <= n + 0 & ... & 1 <= n + 5 & n + 0 <= len the connectives of S & ... & n + 5 <= len the connectives of S ) by A1, A2, NAT_1:12, XXREAL_0:2;

then A3: n + 0 in dom the connectives of S & ... & n + 5 in dom the connectives of S by FINSEQ_3:25;

A4: ( the connectives of S . (n + 0) is_of_type <* the formula-sort of S*>, the formula-sort 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 & the connectives of S . (n + 5) is_of_type {} , the formula-sort of S ) by Def4;

A5: ( In (( the connectives of S . n), the carrier' of S) is_of_type <* the formula-sort of S*>, the formula-sort of S & 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 & ... & In (( the connectives of S . (n + 4)), the carrier' of S) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S & In (( the connectives of S . (n + 5)), the carrier' of S) is_of_type {} , the formula-sort of S ) by A4, A3, FUNCT_1:102, SUBSET_1:def 8;

hereby :: thesis: for A being Formula of L holds

( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) )

let A be Formula of L; :: thesis: ( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds ( ( for a being Element of Args ((In (( the connectives of S . n), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) )

let a be Element of Args ((In (( the connectives of S . (n + 5)), the carrier' of S)),L); :: thesis: ( a = {} implies a / (x,t) = {} )

assume a = {} ; :: thesis: a / (x,t) = {}

then ( dom {} = dom (the_arity_of (In (( the connectives of S . (n + 5)), the carrier' of S))) & dom (the_arity_of (In (( the connectives of S . (n + 5)), the carrier' of S))) = dom (a / (x,t)) ) by MSUALG_6:2;

hence a / (x,t) = {} ; :: thesis: verum

end;assume a = {} ; :: thesis: a / (x,t) = {}

then ( dom {} = dom (the_arity_of (In (( the connectives of S . (n + 5)), the carrier' of S))) & dom (the_arity_of (In (( the connectives of S . (n + 5)), the carrier' of S))) = dom (a / (x,t)) ) by MSUALG_6:2;

hence a / (x,t) = {} ; :: thesis: verum

a / (x,t) = <*(A / (x,t))*> ) & ( for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) ) ) )

hereby :: thesis: for B being Formula of L holds

( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) )

let B be Formula of L; :: thesis: ( ( for a being Element of Args ((In (( the connectives of S . (n + 1)), the carrier' of S)),L) st <*A,B*> = a holds ( ( 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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) )

set o = In (( the connectives of S . n), the carrier' of S);

let a be Element of Args ((In (( the connectives of S . n), the carrier' of S)),L); :: thesis: ( a = <*A*> implies a / (x,t) = <*(A / (x,t))*> )

assume a = <*A*> ; :: thesis: a / (x,t) = <*(A / (x,t))*>

then A6: ( dom a = Seg 1 & a . 1 = A & len a = 1 & dom a = dom (the_arity_of (In (( the connectives of S . n), the carrier' of S))) & dom (the_arity_of (In (( the connectives of S . n), the carrier' of S))) = dom (a / (x,t)) ) by MSUALG_6:2, FINSEQ_1:40, FINSEQ_1:89;

consider j being SortSymbol of S such that

A7: ( j = (the_arity_of (In (( the connectives of S . n), the carrier' of S))) . 1 & ex A being Element of L,j st

( A = a . 1 & (a / (x,t)) . 1 = A / (x,t) ) ) by A6, Def14, FINSEQ_1:1;

( j = the formula-sort of S & len (a / (x,t)) = 1 ) by A5, A6, A7, FINSEQ_1:40, FINSEQ_3:29;

hence a / (x,t) = <*(A / (x,t))*> by A7, A6, FINSEQ_1:40; :: thesis: verum

end;let a be Element of Args ((In (( the connectives of S . n), the carrier' of S)),L); :: thesis: ( a = <*A*> implies a / (x,t) = <*(A / (x,t))*> )

assume a = <*A*> ; :: thesis: a / (x,t) = <*(A / (x,t))*>

then A6: ( dom a = Seg 1 & a . 1 = A & len a = 1 & dom a = dom (the_arity_of (In (( the connectives of S . n), the carrier' of S))) & dom (the_arity_of (In (( the connectives of S . n), the carrier' of S))) = dom (a / (x,t)) ) by MSUALG_6:2, FINSEQ_1:40, FINSEQ_1:89;

consider j being SortSymbol of S such that

A7: ( j = (the_arity_of (In (( the connectives of S . n), the carrier' of S))) . 1 & ex A being Element of L,j st

( A = a . 1 & (a / (x,t)) . 1 = A / (x,t) ) ) by A6, Def14, FINSEQ_1:1;

( j = the formula-sort of S & len (a / (x,t)) = 1 ) by A5, A6, A7, FINSEQ_1:40, FINSEQ_3:29;

hence a / (x,t) = <*(A / (x,t))*> by A7, A6, FINSEQ_1:40; :: thesis: verum

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))*> ) & ( for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) ) ) )

thus 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))*> :: thesis: for z being Element of Union X holds

( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) )

proof

let z be Element of Union X; :: thesis: ( ( for a being Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L) st <*A*> = a holds
let i be natural number ; :: thesis: ( not 1 <= i or not i <= 4 or for a being Element of Args ((In (( the connectives of S . (n + i)), the carrier' of S)),L) st <*A,B*> = a holds

a / (x,t) = <*(A / (x,t)),(B / (x,t))*> )

assume A8: ( 1 <= i & i <= 4 ) ; :: thesis: for a being Element of Args ((In (( the connectives of S . (n + i)), the carrier' of S)),L) st <*A,B*> = a holds

a / (x,t) = <*(A / (x,t)),(B / (x,t))*>

set o = In (( the connectives of S . (n + i)), the carrier' of S);

let a be Element of Args ((In (( the connectives of S . (n + i)), the carrier' of S)),L); :: thesis: ( <*A,B*> = a implies a / (x,t) = <*(A / (x,t)),(B / (x,t))*> )

assume a = <*A,B*> ; :: thesis: a / (x,t) = <*(A / (x,t)),(B / (x,t))*>

then A9: ( dom a = Seg 2 & a . 1 = A & a . 2 = B & len a = 2 & dom a = dom (the_arity_of (In (( the connectives of S . (n + i)), the carrier' of S))) & dom (the_arity_of (In (( the connectives of S . (n + i)), the carrier' of S))) = dom (a / (x,t)) ) by MSUALG_6:2, FINSEQ_1:44, FINSEQ_1:89;

consider j1 being SortSymbol of S such that

A10: ( j1 = (the_arity_of (In (( the connectives of S . (n + i)), the carrier' of S))) . 1 & ex A being Element of L,j1 st

( A = a . 1 & (a / (x,t)) . 1 = A / (x,t) ) ) by A9, Def14, FINSEQ_1:1;

consider j2 being SortSymbol of S such that

A11: ( j2 = (the_arity_of (In (( the connectives of S . (n + i)), the carrier' of S))) . 2 & ex A being Element of L,j2 st

( A = a . 2 & (a / (x,t)) . 2 = A / (x,t) ) ) by A9, Def14, FINSEQ_1:1;

In (( the connectives of S . (n + i)), the carrier' of S) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S by A8, A5;

then ( j1 = the formula-sort of S & j2 = the formula-sort of S ) by A10, A11, FINSEQ_1:44;

hence a / (x,t) = <*(A / (x,t)),(B / (x,t))*> by A9, A10, A11, FINSEQ_3:29, FINSEQ_1:44; :: thesis: verum

end;a / (x,t) = <*(A / (x,t)),(B / (x,t))*> )

assume A8: ( 1 <= i & i <= 4 ) ; :: thesis: for a being Element of Args ((In (( the connectives of S . (n + i)), the carrier' of S)),L) st <*A,B*> = a holds

a / (x,t) = <*(A / (x,t)),(B / (x,t))*>

set o = In (( the connectives of S . (n + i)), the carrier' of S);

let a be Element of Args ((In (( the connectives of S . (n + i)), the carrier' of S)),L); :: thesis: ( <*A,B*> = a implies a / (x,t) = <*(A / (x,t)),(B / (x,t))*> )

assume a = <*A,B*> ; :: thesis: a / (x,t) = <*(A / (x,t)),(B / (x,t))*>

then A9: ( dom a = Seg 2 & a . 1 = A & a . 2 = B & len a = 2 & dom a = dom (the_arity_of (In (( the connectives of S . (n + i)), the carrier' of S))) & dom (the_arity_of (In (( the connectives of S . (n + i)), the carrier' of S))) = dom (a / (x,t)) ) by MSUALG_6:2, FINSEQ_1:44, FINSEQ_1:89;

consider j1 being SortSymbol of S such that

A10: ( j1 = (the_arity_of (In (( the connectives of S . (n + i)), the carrier' of S))) . 1 & ex A being Element of L,j1 st

( A = a . 1 & (a / (x,t)) . 1 = A / (x,t) ) ) by A9, Def14, FINSEQ_1:1;

consider j2 being SortSymbol of S such that

A11: ( j2 = (the_arity_of (In (( the connectives of S . (n + i)), the carrier' of S))) . 2 & ex A being Element of L,j2 st

( A = a . 2 & (a / (x,t)) . 2 = A / (x,t) ) ) by A9, Def14, FINSEQ_1:1;

In (( the connectives of S . (n + i)), the carrier' of S) is_of_type <* the formula-sort of S, the formula-sort of S*>, the formula-sort of S by A8, A5;

then ( j1 = the formula-sort of S & j2 = the formula-sort of S ) by A10, A11, FINSEQ_1:44;

hence a / (x,t) = <*(A / (x,t)),(B / (x,t))*> by A9, A10, A11, FINSEQ_3:29, FINSEQ_1:44; :: thesis: verum

a / (x,t) = <*(A / (x,t))*> ) & ( for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*> ) )

hereby :: thesis: for a being Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L) st <*A*> = a holds

a / (x,t) = <*(A / (x,t))*>

set o = In (( the quantifiers of S . (2,z)), the carrier' of S);a / (x,t) = <*(A / (x,t))*>

set o = In (( the quantifiers of S . (1,z)), the carrier' of S);

let a be Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L); :: thesis: ( a = <*A*> implies a / (x,t) = <*(A / (x,t))*> )

assume a = <*A*> ; :: thesis: a / (x,t) = <*(A / (x,t))*>

then A12: ( dom a = Seg 1 & a . 1 = A & len a = 1 & dom a = dom (the_arity_of (In (( the quantifiers of S . (1,z)), the carrier' of S))) & dom (the_arity_of (In (( the quantifiers of S . (1,z)), the carrier' of S))) = dom (a / (x,t)) ) by MSUALG_6:2, FINSEQ_1:40, FINSEQ_1:89;

consider j being SortSymbol of S such that

A13: ( j = (the_arity_of (In (( the quantifiers of S . (1,z)), the carrier' of S))) . 1 & ex A being Element of L,j st

( A = a . 1 & (a / (x,t)) . 1 = A / (x,t) ) ) by A12, Def14, FINSEQ_1:1;

A14: ( 1 in {1,2} & the quant-sort of S = {1,2} & z in Union X ) by Def5, TARSKI:def 2;

then [1,z] in [: the quant-sort of S,(Union X):] by ZFMISC_1:87;

then In (( the quantifiers of S . (1,z)), the carrier' of S) = the quantifiers of S . (1,z) by SUBSET_1:def 8, FUNCT_2:5;

then In (( the quantifiers of S . (1,z)), the carrier' of S) is_of_type <* the formula-sort of S*>, the formula-sort of S by A14, Def5;

then ( j = the formula-sort of S & len (a / (x,t)) = 1 ) by A12, A13, FINSEQ_1:40, FINSEQ_3:29;

hence a / (x,t) = <*(A / (x,t))*> by A13, A12, FINSEQ_1:40; :: thesis: verum

end;let a be Element of Args ((In (( the quantifiers of S . (1,z)), the carrier' of S)),L); :: thesis: ( a = <*A*> implies a / (x,t) = <*(A / (x,t))*> )

assume a = <*A*> ; :: thesis: a / (x,t) = <*(A / (x,t))*>

then A12: ( dom a = Seg 1 & a . 1 = A & len a = 1 & dom a = dom (the_arity_of (In (( the quantifiers of S . (1,z)), the carrier' of S))) & dom (the_arity_of (In (( the quantifiers of S . (1,z)), the carrier' of S))) = dom (a / (x,t)) ) by MSUALG_6:2, FINSEQ_1:40, FINSEQ_1:89;

consider j being SortSymbol of S such that

A13: ( j = (the_arity_of (In (( the quantifiers of S . (1,z)), the carrier' of S))) . 1 & ex A being Element of L,j st

( A = a . 1 & (a / (x,t)) . 1 = A / (x,t) ) ) by A12, Def14, FINSEQ_1:1;

A14: ( 1 in {1,2} & the quant-sort of S = {1,2} & z in Union X ) by Def5, TARSKI:def 2;

then [1,z] in [: the quant-sort of S,(Union X):] by ZFMISC_1:87;

then In (( the quantifiers of S . (1,z)), the carrier' of S) = the quantifiers of S . (1,z) by SUBSET_1:def 8, FUNCT_2:5;

then In (( the quantifiers of S . (1,z)), the carrier' of S) is_of_type <* the formula-sort of S*>, the formula-sort of S by A14, Def5;

then ( j = the formula-sort of S & len (a / (x,t)) = 1 ) by A12, A13, FINSEQ_1:40, FINSEQ_3:29;

hence a / (x,t) = <*(A / (x,t))*> by A13, A12, FINSEQ_1:40; :: thesis: verum

let a be Element of Args ((In (( the quantifiers of S . (2,z)), the carrier' of S)),L); :: thesis: ( <*A*> = a implies a / (x,t) = <*(A / (x,t))*> )

assume a = <*A*> ; :: thesis: a / (x,t) = <*(A / (x,t))*>

then A15: ( Seg 1 = dom a & a . 1 = A & len a = 1 & dom a = dom (the_arity_of (In (( the quantifiers of S . (2,z)), the carrier' of S))) & dom (the_arity_of (In (( the quantifiers of S . (2,z)), the carrier' of S))) = dom (a / (x,t)) ) by MSUALG_6:2, FINSEQ_1:40, FINSEQ_1:89;

consider j being SortSymbol of S such that

A16: ( j = (the_arity_of (In (( the quantifiers of S . (2,z)), the carrier' of S))) . 1 & ex A being Element of L,j st

( A = a . 1 & (a / (x,t)) . 1 = A / (x,t) ) ) by A15, Def14, FINSEQ_1:1;

A17: ( 2 in {1,2} & the quant-sort of S = {1,2} & z in Union X ) by Def5, TARSKI:def 2;

then [2,z] in [: the quant-sort of S,(Union X):] by ZFMISC_1:87;

then In (( the quantifiers of S . (2,z)), the carrier' of S) = the quantifiers of S . (2,z) by SUBSET_1:def 8, FUNCT_2:5;

then In (( the quantifiers of S . (2,z)), the carrier' of S) is_of_type <* the formula-sort of S*>, the formula-sort of S by A17, Def5;

then ( j = the formula-sort of S & len (a / (x,t)) = 1 ) by A15, A16, FINSEQ_1:40, FINSEQ_3:29;

hence a / (x,t) = <*(A / (x,t))*> by A16, A15, FINSEQ_1:40; :: thesis: verum