let n be natural non empty number ; :: thesis: for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being empty-yielding GeneratorSet of T
for S being non empty non void b1 -extension n PC-correct QC-correct QCLangSignature over Union X
for Y being empty-yielding 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 empty-yielding GeneratorSet of T
for S being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X
for Y being empty-yielding 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 empty-yielding GeneratorSet of T
for S being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X
for Y being empty-yielding 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 empty-yielding GeneratorSet of T; :: thesis: for S being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X
for Y being empty-yielding X -tolerating ManySortedSet of the carrier of S
for L being non-empty Language of Y,S
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 empty-yielding 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 empty-yielding 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 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 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_3:29;
hence a / (x,t) = <*(A / (x,t))*> by A7, A6, FINSEQ_1:40; :: 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 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;
hence a / (x,t) = <*(A / (x,t)),(B / (x,t))*> by A9, A10, A11, FINSEQ_3:29, FINSEQ_1:44; :: 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 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_3:29;
hence a / (x,t) = <*(A / (x,t))*> by A13, A12, FINSEQ_1:40; :: 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 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_3:29;
hence a / (x,t) = <*(A / (x,t))*> by A16, A15, FINSEQ_1:40; :: thesis: verum