set O = {0,1,2,3,4,5} \/ [:{1,2},X:];

set a = (({1,2,3,4} --> <*0,0*>) \/ (({0} \/ [:{1,2},X:]) --> <*0*>)) \/ ({5} --> {});

set r = ({0,1,2,3,4,5} \/ [:{1,2},X:]) --> 0;

A1: ( dom ({1,2,3,4} --> <*0,0*>) = {1,2,3,4} & dom ({5} --> {}) = {5} & dom (({0} \/ [:{1,2},X:]) --> <*0*>) = {0} \/ [:{1,2},X:] ) ;

B1: [:{1,2},X:] misses {0,1,2,3,4,5}

A4: dom aa = {1,2,3,4} \/ ({0} \/ [:{1,2},X:]) by A1, XTUPLE_0:23

.= ({0} \/ {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}

A6: dom a = ({0,1,2,3,4} \/ [:{1,2},X:]) \/ {5} by A1, A4, XTUPLE_0:23

.= ({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 {0} by TARSKI:def 1;

( <*00*> in {0} * & <*00,00*> in {0} * ) by FINSEQ_1:def 11;

then ( rng ({1,2,3,4} --> <*0,0*>) c= {0} * & rng (({0} \/ [:{1,2},X:]) --> <*0*>) c= {0} * ) by ZFMISC_1:31;

then ( (rng ({1,2,3,4} --> <*0,0*>)) \/ (rng (({0} \/ [:{1,2},X:]) --> <*0*>)) c= {0} * & <*> {0} in {0} * ) by FINSEQ_1:def 11, XBOOLE_1:8;

then ( rng aa c= {0} * & rng ({5} --> {}) c= {0} * ) by RELAT_1:12;

then (rng aa) \/ (rng ({5} --> {})) c= {0} * by XBOOLE_1:8;

then rng a c= {0} * by RELAT_1:12;

then reconsider a = a as Function of ({0,1,2,3,4,5} \/ [:{1,2},X:]),({0} *) by A6, FUNCT_2:2;

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} ;

( 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 XBOOLE_1:1, FINSEQ_1:def 4;

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 B2, XBOOLE_1:13, FINSEQ_1:31;

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

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 A7, XREAL_1:235;

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 )

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 Def7, XBOOLE_1:7;

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 B1, B3, XBOOLE_1:64; :: 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

set a = (({1,2,3,4} --> <*0,0*>) \/ (({0} \/ [:{1,2},X:]) --> <*0*>)) \/ ({5} --> {});

set r = ({0,1,2,3,4,5} \/ [:{1,2},X:]) --> 0;

A1: ( dom ({1,2,3,4} --> <*0,0*>) = {1,2,3,4} & dom ({5} --> {}) = {5} & dom (({0} \/ [:{1,2},X:]) --> <*0*>) = {0} \/ [:{1,2},X:] ) ;

B1: [:{1,2},X:] misses {0,1,2,3,4,5}

proof

{1,2,3,4} misses {0} \/ [:{1,2},X:]
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;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

proof

then reconsider aa = ({1,2,3,4} --> <*0,0*>) \/ (({0} \/ [:{1,2},X:]) --> <*0*>) as Function by A1, GRFUNC_1:13;
assume
{1,2,3,4} meets {0} \/ [:{1,2},X:]
; :: thesis: contradiction

then consider x being object such that

A2: ( x in {1,2,3,4} & x in {0} \/ [:{1,2},X:] ) by XBOOLE_0:3;

( x in {0} or x in [:{1,2},X:] ) by A2, XBOOLE_0:def 3;

then consider y, z being object such that

A3: ( y in {1,2} & z in X & x = [y,z] ) by A2, ENUMSET1:def 2;

thus contradiction by A2, A3, ENUMSET1:def 2; :: thesis: verum

end;then consider x being object such that

A2: ( x in {1,2,3,4} & x in {0} \/ [:{1,2},X:] ) by XBOOLE_0:3;

( x in {0} or x in [:{1,2},X:] ) by A2, XBOOLE_0:def 3;

then consider y, z being object such that

A3: ( y in {1,2} & z in X & x = [y,z] ) by A2, ENUMSET1:def 2;

thus contradiction by A2, A3, ENUMSET1:def 2; :: thesis: verum

A4: dom aa = {1,2,3,4} \/ ({0} \/ [:{1,2},X:]) by A1, XTUPLE_0:23

.= ({0} \/ {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

then reconsider a = (({1,2,3,4} --> <*0,0*>) \/ (({0} \/ [:{1,2},X:]) --> <*0*>)) \/ ({5} --> {}) as Function by A1, A4, GRFUNC_1:13;
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 A5, TARSKI:def 1;

then ( 5 in {0,1,2,3,4} or 5 in [:{1,2},X:] ) by A5, XBOOLE_0:def 3;

hence contradiction by ENUMSET1:def 3; :: thesis: verum

end;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 A5, TARSKI:def 1;

then ( 5 in {0,1,2,3,4} or 5 in [:{1,2},X:] ) by A5, XBOOLE_0:def 3;

hence contradiction by ENUMSET1:def 3; :: thesis: verum

A6: dom a = ({0,1,2,3,4} \/ [:{1,2},X:]) \/ {5} by A1, A4, XTUPLE_0:23

.= ({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 {0} by TARSKI:def 1;

( <*00*> in {0} * & <*00,00*> in {0} * ) by FINSEQ_1:def 11;

then ( rng ({1,2,3,4} --> <*0,0*>) c= {0} * & rng (({0} \/ [:{1,2},X:]) --> <*0*>) c= {0} * ) by ZFMISC_1:31;

then ( (rng ({1,2,3,4} --> <*0,0*>)) \/ (rng (({0} \/ [:{1,2},X:]) --> <*0*>)) c= {0} * & <*> {0} in {0} * ) by FINSEQ_1:def 11, XBOOLE_1:8;

then ( rng aa c= {0} * & rng ({5} --> {}) c= {0} * ) by RELAT_1:12;

then (rng aa) \/ (rng ({5} --> {})) c= {0} * by XBOOLE_1:8;

then rng a c= {0} * by RELAT_1:12;

then reconsider a = a as Function of ({0,1,2,3,4,5} \/ [:{1,2},X:]),({0} *) by A6, FUNCT_2:2;

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} ;

( 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 XBOOLE_1:1, FINSEQ_1:def 4;

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 B2, XBOOLE_1:13, FINSEQ_1:31;

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

take L = QCLangSignature(# {0},({0,1,2,3,4,5} \/ [:{1,2},X:]),a,r,(In (0,{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 )
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;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

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 A7, XREAL_1:235;

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

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 )
let x be object ; :: according to FUNCT_1:def 4 :: thesis: for b_{1} being object holds

( not x in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) or not b_{1} 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)}) . b_{1} or x = b_{1} )

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 A9, FUNCT_1:49;

A12: ( not not x = n + 0 & ... & not x = n + 5 & not not y = n + 0 & ... & not y = n + 5 ) by A10, ENUMSET1:def 4;

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 A13, A14;

then ( c . x = i & c . y = j ) by A8, A13, A14;

hence x = y by A11, A13, A14; :: thesis: verum

end;( not x in dom ( the connectives of L | {n,(n + 1),(n + 2),(n + 3),(n + 4),(n + 5)}) or not b

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 A9, FUNCT_1:49;

A12: ( not not x = n + 0 & ... & not x = n + 5 & not not y = n + 0 & ... & not y = n + 5 ) by A10, ENUMSET1:def 4;

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 A13, A14;

then ( c . x = i & c . y = j ) by A8, A13, A14;

hence x = y by A11, A13, A14; :: thesis: verum

proof

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 )
not not 0 = 0 & ... & not 0 = 5
;

then A15: c . (n + 0) = 0 by A8;

( 00 in {0} \/ [:{1,2},X:] & <*0*> in {<*0*>} ) by XBOOLE_0:def 3, TARSKI:def 1;

then [0,<*0*>] in ({0} \/ [:{1,2},X:]) --> <*0*> by ZFMISC_1:106;

then [0,<*0*>] in aa by XBOOLE_0:def 3;

then [0,<*0*>] in a by XBOOLE_0:def 3;

hence the Arity of L . ( the connectives of L . n) = <*00*> by A15, FUNCT_1:1

.= <* 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;then A15: c . (n + 0) = 0 by A8;

( 00 in {0} \/ [:{1,2},X:] & <*0*> in {<*0*>} ) by XBOOLE_0:def 3, TARSKI:def 1;

then [0,<*0*>] in ({0} \/ [:{1,2},X:]) --> <*0*> by ZFMISC_1:106;

then [0,<*0*>] in aa by XBOOLE_0:def 3;

then [0,<*0*>] in a by XBOOLE_0:def 3;

hence the Arity of L . ( the connectives of L . n) = <*00*> by A15, FUNCT_1:1

.= <* 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

proof

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
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 A16, FUNCT_1:1; :: 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;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 A16, FUNCT_1:1; :: 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

proof

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
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} & <*0,0*> in {<*0,0*>} ) by TARSKI:def 1, ENUMSET1:def 2;

then [(c . (n + i)),<*0,0*>] in {1,2,3,4} --> <*0,0*> by ZFMISC_1:106;

then [(c . (n + i)),<*0,0*>] in aa by XBOOLE_0:def 3;

then [(c . (n + i)),<*0,0*>] 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;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} & <*0,0*> in {<*0,0*>} ) by TARSKI:def 1, ENUMSET1:def 2;

then [(c . (n + i)),<*0,0*>] in {1,2,3,4} --> <*0,0*> by ZFMISC_1:106;

then [(c . (n + i)),<*0,0*>] in aa by XBOOLE_0:def 3;

then [(c . (n + i)),<*0,0*>] 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

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 Def7, XBOOLE_1:7;

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 B1, B3, XBOOLE_1:64; :: 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] & <*0*> in {<*0*>} ) by A19, A18, FUNCT_1:18, TARSKI:def 1, ZFMISC_1:87;

then ( the quantifiers of L . (q,x) in {0} \/ [:{1,2},X:] & <*0*> in {<*0*>} ) by A20, XBOOLE_0:def 3;

then [( the quantifiers of L . (q,x)),<*0*>] in ({0} \/ [:{1,2},X:]) --> <*0*> by ZFMISC_1:106;

then [( the quantifiers of L . (q,x)),<*0*>] in aa by XBOOLE_0:def 3;

then A21: [( the quantifiers of L . (q,x)),<*0*>] 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

end;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] & <*0*> in {<*0*>} ) by A19, A18, FUNCT_1:18, TARSKI:def 1, ZFMISC_1:87;

then ( the quantifiers of L . (q,x) in {0} \/ [:{1,2},X:] & <*0*> in {<*0*>} ) by A20, XBOOLE_0:def 3;

then [( the quantifiers of L . (q,x)),<*0*>] in ({0} \/ [:{1,2},X:]) --> <*0*> by ZFMISC_1:106;

then [( the quantifiers of L . (q,x)),<*0*>] in aa by XBOOLE_0:def 3;

then A21: [( the quantifiers of L . (q,x)),<*0*>] 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 A21, FUNCT_1:1

.= <* 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;.= <* 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