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 b1 -extension n PC-correct QC-correct QCLangSignature over Union X
for Y being V3() b3 -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() b2 -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() b1 -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 ;
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 ;
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 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;
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
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))*> ) ) ) )
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 ;
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 ;
( j = the formula-sort of S & len (a / (x,t)) = 1 ) by ;
hence a / (x,t) = <*(A / (x,t))*> by ; :: thesis: verum
end;
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
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 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 ;
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 ;
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 ;
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 ;
hence a / (x,t) = <*(A / (x,t)),(B / (x,t))*> by ; :: thesis: verum
end;
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
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 . (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 ;
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 ;
A14: ( 1 in {1,2} & the quant-sort of S = {1,2} & z in Union X ) by ;
then [1,z] in [: the quant-sort of S,():] by ZFMISC_1:87;
then In (( the quantifiers of S . (1,z)), the carrier' of S) = the quantifiers of S . (1,z) by ;
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 ;
then ( j = the formula-sort of S & len (a / (x,t)) = 1 ) by ;
hence a / (x,t) = <*(A / (x,t))*> by ; :: thesis: verum
end;
set o = In (( the quantifiers of S . (2,z)), the carrier' of S);
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 ;
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 ;
A17: ( 2 in {1,2} & the quant-sort of S = {1,2} & z in Union X ) by ;
then [2,z] in [: the quant-sort of S,():] by ZFMISC_1:87;
then In (( the quantifiers of S . (2,z)), the carrier' of S) = the quantifiers of S . (2,z) by ;
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 ;
then ( j = the formula-sort of S & len (a / (x,t)) = 1 ) by ;
hence a / (x,t) = <*(A / (x,t))*> by ; :: thesis: verum