set O = {0,1,2,3,4,5} \/ [:{1,2},X:];
set a = (({1,2,3,4} --> ) \/ (( \/ [:{1,2},X:]) --> )) \/ ();
set r = ({0,1,2,3,4,5} \/ [:{1,2},X:]) --> 0;
A1: ( dom ({1,2,3,4} --> ) = {1,2,3,4} & dom () = {5} & dom (( \/ [:{1,2},X:]) --> ) = \/ [:{1,2},X:] ) ;
B1: [:{1,2},X:] misses {0,1,2,3,4,5}
proof
assume [:{1,2},X:] meets {0,1,2,3,4,5} ; :: thesis: contradiction
then consider x being object such that
A2: ( x in {0,1,2,3,4,5} & x in [:{1,2},X:] ) by XBOOLE_0:3;
thus contradiction by A2, ENUMSET1:def 4; :: thesis: verum
end;
{1,2,3,4} misses \/ [:{1,2},X:]
proof
assume {1,2,3,4} meets \/ [:{1,2},X:] ; :: thesis: contradiction
then consider x being object such that
A2: ( x in {1,2,3,4} & x in \/ [:{1,2},X:] ) by XBOOLE_0:3;
( x in or x in [:{1,2},X:] ) by ;
then consider y, z being object such that
A3: ( y in {1,2} & z in X & x = [y,z] ) by ;
thus contradiction by A2, A3, ENUMSET1:def 2; :: thesis: verum
end;
then reconsider aa = ({1,2,3,4} --> ) \/ (( \/ [:{1,2},X:]) --> ) as Function by ;
A4: dom aa = {1,2,3,4} \/ ( \/ [:{1,2},X:]) by
.= ( \/ {1,2,3,4}) \/ [:{1,2},X:] by XBOOLE_1:4
.= {0,1,2,3,4} \/ [:{1,2},X:] by ENUMSET1:7 ;
{0,1,2,3,4} \/ [:{1,2},X:] misses {5}
proof
assume {0,1,2,3,4} \/ [:{1,2},X:] meets {5} ; :: thesis: contradiction
then consider x being object such that
A5: ( x in {0,1,2,3,4} \/ [:{1,2},X:] & x in {5} ) by XBOOLE_0:3;
x = 5 by ;
then ( 5 in {0,1,2,3,4} or 5 in [:{1,2},X:] ) by ;
hence contradiction by ENUMSET1:def 3; :: thesis: verum
end;
then reconsider a = (({1,2,3,4} --> ) \/ (( \/ [:{1,2},X:]) --> )) \/ () as Function by ;
A6: dom a = ({0,1,2,3,4} \/ [:{1,2},X:]) \/ {5} by
.= ({5} \/ {0,1,2,3,4}) \/ [:{1,2},X:] by XBOOLE_1:4
.= {0,1,2,3,4,5} \/ [:{1,2},X:] by ENUMSET1:15 ;
reconsider 00 = 0 as Element of by TARSKI:def 1;
( <*00*> in * & <*00,00*> in * ) by FINSEQ_1:def 11;
then ( rng ({1,2,3,4} --> ) c= * & rng (( \/ [:{1,2},X:]) --> ) c= * ) by ZFMISC_1:31;
then ( (rng ({1,2,3,4} --> )) \/ (rng (( \/ [:{1,2},X:]) --> )) c= * & <*> in * ) by ;
then ( rng aa c= * & rng () c= * ) by RELAT_1:12;
then (rng aa) \/ (rng ()) c= * by XBOOLE_1:8;
then rng a c= * by RELAT_1:12;
then reconsider a = a as Function of ({0,1,2,3,4,5} \/ [:{1,2},X:]),() by ;
reconsider r = ({0,1,2,3,4,5} \/ [:{1,2},X:]) --> 0 as Function of ({0,1,2,3,4,5} \/ [:{1,2},X:]), ;
( 0 in {0,1,2,3,4,5} & 1 in {0,1,2,3,4,5} & 2 in {0,1,2,3,4,5} & 3 in {0,1,2,3,4,5} & 4 in {0,1,2,3,4,5} & 5 in {0,1,2,3,4,5} ) by ENUMSET1:def 4;
then reconsider o0 = 0 , o1 = 1, o2 = 2, o3 = 3, o4 = 4, o5 = 5 as Element of {0,1,2,3,4,5} \/ [:{1,2},X:] by XBOOLE_0:def 3;
set p = the n -' 1 -element FinSequence of {0,1,2,3,4,5};
B2: ( rng the n -' 1 -element FinSequence of {0,1,2,3,4,5} c= {0,1,2,3,4,5} & {0,1,2,3,4,5} c= {0,1,2,3,4,5} \/ [:{1,2},X:] ) by XBOOLE_1:7;
then reconsider p = the n -' 1 -element FinSequence of {0,1,2,3,4,5} as FinSequence of {0,1,2,3,4,5} \/ [:{1,2},X:] by ;
set c6 = <*o0,o1,o2,o3,o4,o5*>;
reconsider c = p ^ <*o0,o1,o2,o3,o4,o5*> as FinSequence of {0,1,2,3,4,5} \/ [:{1,2},X:] ;
rng <*o0,o1,o2,o3,o4,o5*> = {0,1,2,3,4,5} by AOFA_A00:21;
then B3: ( rng c = (rng p) \/ (rng <*o0,o1,o2,o3,o4,o5*>) & (rng p) \/ (rng <*o0,o1,o2,o3,o4,o5*>) c= {0,1,2,3,4,5} \/ {0,1,2,3,4,5} & {0,1,2,3,4,5} \/ {0,1,2,3,4,5} = {0,1,2,3,4,5} ) by ;
n > 0 ;
then A7: n >= 0 + 1 by NAT_1:13;
A8: for i being natural number st not not i = 0 & ... & not i = 5 holds
c . (n + i) = i
proof
let i be natural number ; :: thesis: ( not not i = 0 & ... & not i = 5 implies c . (n + i) = i )
assume not not i = 0 & ... & not i = 5 ; :: thesis: c . (n + i) = i
then not ( not i = 0 or not c . (n + 0) = <*o0,o1,o2,o3,o4,o5*> . (0 + 1) ) & ... & ( not i = 5 or not c . (n + 5) = <*o0,o1,o2,o3,o4,o5*> . (5 + 1) ) ;
hence c . (n + i) = i by AOFA_A00:20; :: thesis: verum
end;
take L = QCLangSignature(# ,({0,1,2,3,4,5} \/ [:{1,2},X:]),a,r,(In (0,)),c,{1,2},(incl ([:{1,2},X:],({0,1,2,3,4,5} \/ [:{1,2},X:]))) #); :: thesis: ( not L is void & not L is empty & L is n PC-correct & L is QC-correct )
thus not the carrier' of L is empty ; :: according to STRUCT_0:def 13 :: thesis: ( not L is empty & L is n PC-correct & L is QC-correct )
thus not the carrier of L is empty ; :: according to STRUCT_0:def 1 :: thesis: ( L is n PC-correct & L is QC-correct )
( len <*o0,o1,o2,o3,o4,o5*> = 5 + 1 & len p = n -' 1 ) by CARD_1:def 7;
then ( (len p) + (len <*o0,o1,o2,o3,o4,o5*>) = (n -' 1) + (1 + 5) & (n -' 1) + (1 + 5) = ((n -' 1) + 1) + 5 & n is Real & 1 is Real ) ;
then (len p) + (len <*o0,o1,o2,o3,o4,o5*>) = n + 5 by ;
hence len the connectives of L >= n + 5 by FINSEQ_1:22; :: according to AOFA_L00:def 4 :: thesis: ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} is one-to-one & the connectives of L . n is_of_type <* the formula-sort of L*>, the formula-sort of L & the connectives of L . (n + 5) is_of_type {} , the formula-sort of L & the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & L is QC-correct )
set N = {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)};
thus the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} is one-to-one :: thesis: ( the connectives of L . n is_of_type <* the formula-sort of L*>, the formula-sort of L & the connectives of L . (n + 5) is_of_type {} , the formula-sort of L & the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & L is QC-correct )
proof
let x be object ; :: according to FUNCT_1:def 4 :: thesis: for b1 being object holds
( not x in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) or not b1 in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) or not ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x = ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . b1 or x = b1 )

let y be object ; :: thesis: ( not x in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) or not y in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) or not ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x = ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . y or x = y )
assume A9: ( x in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) & y in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) & ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x = ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . y ) ; :: thesis: x = y
then A10: ( x in {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} & y in {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)} ) by RELAT_1:57;
then A11: ( c . x = (c | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x & (c | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) . x = c . y ) by ;
A12: ( not not x = n + 0 & ... & not x = n + 5 & not not y = n + 0 & ... & not y = n + 5 ) by ;
then consider i being Nat such that
A13: ( 0 <= i & i <= 5 & x = n + i ) ;
consider j being Nat such that
A14: ( 0 <= j & j <= 5 & y = n + j ) by A12;
( not not i = 0 & ... & not i = 5 & not not j = 0 & ... & not j = 5 ) by ;
then ( c . x = i & c . y = j ) by A8, A13, A14;
hence x = y by ; :: thesis: verum
end;
thus the connectives of L . n is_of_type <* the formula-sort of L*>, the formula-sort of L :: thesis: ( the connectives of L . (n + 5) is_of_type {} , the formula-sort of L & the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & L is QC-correct )
proof
not not 0 = 0 & ... & not 0 = 5 ;
then A15: c . (n + 0) = 0 by A8;
( 00 in \/ [:{1,2},X:] & in ) by ;
then [] in ( \/ [:{1,2},X:]) --> by ZFMISC_1:106;
then [] in aa by XBOOLE_0:def 3;
then [] in a by XBOOLE_0:def 3;
hence the Arity of L . ( the connectives of L . n) = <*00*> by
.= <* the formula-sort of L*> ;
:: according to AOFA_A00:def 8 :: thesis: the ResultSort of L . ( the connectives of L . n) = the formula-sort of L
thus the ResultSort of L . ( the connectives of L . n) = 00
.= the formula-sort of L ; :: thesis: verum
end;
thus the connectives of L . (n + 5) is_of_type {} , the formula-sort of L :: thesis: ( the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & L is QC-correct )
proof
not not 0 = 5 & ... & not 5 = 5 ;
then A16: c . (n + 5) = 5 by A8;
( 5 in {5} & {} in ) by TARSKI:def 1;
then [5,{}] in {5} --> {} by ZFMISC_1:106;
then [5,{}] in a by XBOOLE_0:def 3;
hence the Arity of L . ( the connectives of L . (n + 5)) = {} by ; :: according to AOFA_A00:def 8 :: thesis: the ResultSort of L . ( the connectives of L . (n + 5)) = the formula-sort of L
thus the ResultSort of L . ( the connectives of L . (n + 5)) = 00
.= the formula-sort of L ; :: thesis: verum
end;
thus the connectives of L . (n + 1) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 4) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L :: thesis: L is QC-correct
proof
let i be natural number ; :: thesis: ( not 1 <= i or not i <= 4 or the connectives of L . (n + i) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L )
assume ( 1 <= i & i <= 4 ) ; :: thesis: the connectives of L . (n + i) is_of_type <* the formula-sort of L, the formula-sort of L*>, the formula-sort of L
then A17: not not i = 1 & ... & not i = 4 ;
not ( not i = 1 or not c . (n + 1) = 1 ) & ... & ( not i = 4 or not c . (n + 4) = 4 ) by A17;
then ( c . (n + i) in {1,2,3,4} & in ) by ;
then [(c . (n + i)),] in {1,2,3,4} --> by ZFMISC_1:106;
then [(c . (n + i)),] in aa by XBOOLE_0:def 3;
then [(c . (n + i)),] in a by XBOOLE_0:def 3;
hence the Arity of L . ( the connectives of L . (n + i)) = <*00,0*> by FUNCT_1:1
.= <* the formula-sort of L,00*>
.= <* the formula-sort of L, the formula-sort of L*> ;
:: according to AOFA_A00:def 8 :: thesis: the ResultSort of L . ( the connectives of L . (n + i)) = the formula-sort of L
thus the ResultSort of L . ( the connectives of L . (n + i)) = 00
.= the formula-sort of L ; :: thesis: verum
end;
thus the quant-sort of L = {1,2} ; :: according to AOFA_L00:def 5 :: thesis: ( the quantifiers of L is one-to-one & rng the quantifiers of L misses rng the connectives of L & ( for q, x being object st q in the quant-sort of L & x in X holds
the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L ) )

A18: the quantifiers of L = id [:{1,2},X:] by ;
hence the quantifiers of L is one-to-one ; :: thesis: ( rng the quantifiers of L misses rng the connectives of L & ( for q, x being object st q in the quant-sort of L & x in X holds
the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L ) )

rng the quantifiers of L c= [:{1,2},X:] by A18;
hence rng the quantifiers of L misses rng the connectives of L by ; :: thesis: for q, x being object st q in the quant-sort of L & x in X holds
the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L

hereby :: thesis: verum
let q, x be object ; :: thesis: ( q in the quant-sort of L & x in X implies the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L )
assume A19: ( q in the quant-sort of L & x in X ) ; :: thesis: the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L
then A20: [q,x] in [: the quant-sort of L,X:] by ZFMISC_1:87;
( the quantifiers of L . (q,x) = [q,x] & in ) by ;
then ( the quantifiers of L . (q,x) in \/ [:{1,2},X:] & in ) by ;
then [( the quantifiers of L . (q,x)),] in ( \/ [:{1,2},X:]) --> by ZFMISC_1:106;
then [( the quantifiers of L . (q,x)),] in aa by XBOOLE_0:def 3;
then A21: [( the quantifiers of L . (q,x)),] in a by XBOOLE_0:def 3;
thus the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L :: thesis: verum
proof
thus the Arity of L . ( the quantifiers of L . (q,x)) = <*00*> by
.= <* the formula-sort of L*> ; :: according to AOFA_A00:def 8 :: thesis: the ResultSort of L . ( the quantifiers of L . (q,x)) = the formula-sort of L
thus the ResultSort of L . ( the quantifiers of L . (q,x)) = 00
.= the formula-sort of L ; :: thesis: verum
end;
end;