defpred S₁[ object , object ] means ex y1, y2, y3 being set st
( y1 in A & y2 in A & y3 in A & ( ( $1 = [1,<*y1*>] & $2 = [0,<*y1,y1*>] ) or ( $1 = [2,<*y1,y2,y3*>] & $2 = [0,<*y1,y3*>] ) ) );
defpred S₂[ object , object ] means ex y1, y2, y3 being set st
( y1 in A & y2 in A & y3 in A & ( ( $1 = [1,<*y1*>] & $2 = {} ) or ( $1 = [2,<*y1,y2,y3*>] & $2 = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) );
A1: for x being object st x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] holds
ex y being object st
( y in [:{0},(2 -tuples_on A):] * & S₂[x,y] )

let x be object ; :: thesis:
assume A2: x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; :: thesis:

per cases by A2, XBOOLE_0:def 3;

suppose A3: x in [:{1},(1 -tuples_on A):] ; :: thesis:

then x `2 in 1 -tuples_on A by MCART_1:10;
then A4: x `2 in { s where s is Element of A * : len s = 1 } by FINSEQ_2:def 4;
take y = {} ; :: thesis:
thus y in [:{0},(2 -tuples_on A):] * by FINSEQ_1:49; :: thesis:
consider s being Element of A * such that
A5: x `2 = s and
A6: len s = 1 by A4;
take y1 = s . 1; :: thesis:
take y2 = s . 1; :: thesis:
take y3 = s . 1; :: thesis:
A7: s = <*y1*> by A6, FINSEQ_1:40;
then ( y1 in {y1} & rng s = {y1} ) by FINSEQ_1:39, TARSKI:def 1;
hence ( y1 in A & y2 in A & y3 in A ) ; :: thesis:
x `1 in {1} by A3, MCART_1:10;
then x `1 = 1 by TARSKI:def 1;
hence ( ( x = [1,<*y1*>] & y = {} ) or ( x = [2,<*y1,y2,y3*>] & y = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) by A3, A5, A7, MCART_1:21; :: thesis:

end;

suppose A8: x in [:{2},(3 -tuples_on A):] ; :: thesis:

then x `2 in 3 -tuples_on A by MCART_1:10;
then x `2 in { s where s is Element of A * : len s = 3 } by FINSEQ_2:def 4;
then consider s being Element of A * such that
A9: x `2 = s and
A10: len s = 3 ;
set y1 = s . 1;
set y2 = s . 2;
set y3 = s . 3;
A11: s = <*(s . 1),(s . 2),(s . 3)*> by A10, FINSEQ_1:45;
then A12: rng s = {(s . 1),(s . 2),(s . 3)} by FINSEQ_2:128;
then reconsider B = A as non empty set ;
take y = <*[0,<*(s . 2),(s . 3)*>],[0,<*(s . 1),(s . 2)*>]*>; :: thesis:
A13: s . 2 in {(s . 1),(s . 2),(s . 3)} by ENUMSET1:def 1;
A14: s . 1 in {(s . 1),(s . 2),(s . 3)} by ENUMSET1:def 1;
then A15: ( 0 in {0} & <*(s . 1),(s . 2)*> in 2 -tuples_on B ) by A13, A12, FINSEQ_2:101, TARSKI:def 1;
A16: s . 3 in {(s . 1),(s . 2),(s . 3)} by ENUMSET1:def 1;
then <*(s . 2),(s . 3)*> in 2 -tuples_on B by A13, A12, FINSEQ_2:101;
then reconsider z1 = [0,<*(s . 2),(s . 3)*>], z2 = [0,<*(s . 1),(s . 2)*>] as Element of [:{0},(2 -tuples_on B):] by A15, ZFMISC_1:87;
y = <*z1*> ^ <*z2*> by FINSEQ_1:def 9;
hence y in [:{0},(2 -tuples_on A):] * by FINSEQ_1:def 11; :: thesis:
take s . 1 ; :: thesis:
take s . 2 ; :: thesis:
take s . 3 ; :: thesis:
thus ( s . 1 in A & s . 2 in A & s . 3 in A ) by A14, A13, A16, A12; :: thesis:
x `1 in {2} by A8, MCART_1:10;
then x `1 = 2 by TARSKI:def 1;
hence ( ( x = [1,<*(s . 1)*>] & y = {} ) or ( x = [2,<*(s . 1),(s . 2),(s . 3)*>] & y = <*[0,<*(s . 2),(s . 3)*>],[0,<*(s . 1),(s . 2)*>]*> ) ) by A8, A9, A11, MCART_1:21; :: thesis:

end;

consider Ar being Function such that
A17: ( dom Ar = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & rng Ar c= [:{0},(2 -tuples_on A):] * ) and
A18: for x being object st x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] holds
S₂[x,Ar . x] from FUNCT_1:sch 6(A1);
reconsider Ar = Ar as Function of ([:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):]),([:{0},(2 -tuples_on A):] *) by A17, FUNCT_2:2;
A19: for x being object st x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] holds
ex y being object st
( y in [:{0},(2 -tuples_on A):] & S₁[x,y] )

proof

let x be object ; :: thesis:
assume A20: x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; :: thesis:

per cases by A20, XBOOLE_0:def 3;

suppose A21: x in [:{1},(1 -tuples_on A):] ; :: thesis:

then x `2 in 1 -tuples_on A by MCART_1:10;
then x `2 in { s where s is Element of A * : len s = 1 } by FINSEQ_2:def 4;
then consider s being Element of A * such that
A22: x `2 = s and
A23: len s = 1 ;
set y1 = s . 1;
set y2 = s . 1;
set y3 = s . 1;
A24: s = <*(s . 1)*> by A23, FINSEQ_1:40;
then A25: ( s . 1 in {(s . 1)} & rng s = {(s . 1)} ) by FINSEQ_1:39, TARSKI:def 1;
take y = [0,<*(s . 1),(s . 1)*>]; :: thesis:
reconsider B = A as non empty set by A24;
reconsider y1 = s . 1 as Element of B by A25;
( 0 in {0} & <*y1,y1*> in 2 -tuples_on B ) by FINSEQ_2:101, TARSKI:def 1;
hence y in [:{0},(2 -tuples_on A):] by ZFMISC_1:87; :: thesis:
take y1 ; :: thesis:
take s . 1 ; :: thesis:
take s . 1 ; :: thesis:
thus ( y1 in A & s . 1 in A & s . 1 in A ) by A25; :: thesis:
x `1 in {1} by A21, MCART_1:10;
then x `1 = 1 by TARSKI:def 1;
hence ( ( x = [1,<*y1*>] & y = [0,<*y1,y1*>] ) or ( x = [2,<*y1,(s . 1),(s . 1)*>] & y = [0,<*y1,(s . 1)*>] ) ) by A21, A22, A24, MCART_1:21; :: thesis:

end;

suppose A26: x in [:{2},(3 -tuples_on A):] ; :: thesis:

then x `2 in 3 -tuples_on A by MCART_1:10;
then x `2 in { s where s is Element of A * : len s = 3 } by FINSEQ_2:def 4;
then consider s being Element of A * such that
A27: x `2 = s and
A28: len s = 3 ;
set y1 = s . 1;
set y2 = s . 2;
set y3 = s . 3;
A29: s = <*(s . 1),(s . 2),(s . 3)*> by A28, FINSEQ_1:45;
then A30: rng s = {(s . 1),(s . 2),(s . 3)} by FINSEQ_2:128;
then reconsider B = A as non empty set ;
take y = [0,<*(s . 1),(s . 3)*>]; :: thesis:
A31: ( s . 1 in {(s . 1),(s . 2),(s . 3)} & s . 3 in {(s . 1),(s . 2),(s . 3)} ) by ENUMSET1:def 1;
then ( 0 in {0} & <*(s . 1),(s . 3)*> in 2 -tuples_on B ) by A30, FINSEQ_2:101, TARSKI:def 1;
hence y in [:{0},(2 -tuples_on A):] by ZFMISC_1:87; :: thesis:
take s . 1 ; :: thesis:
take s . 2 ; :: thesis:
take s . 3 ; :: thesis:
s . 2 in {(s . 1),(s . 2),(s . 3)} by ENUMSET1:def 1;
hence ( s . 1 in A & s . 2 in A & s . 3 in A ) by A31, A30; :: thesis:
x `1 in {2} by A26, MCART_1:10;
then x `1 = 2 by TARSKI:def 1;
hence ( ( x = [1,<*(s . 1)*>] & y = [0,<*(s . 1),(s . 1)*>] ) or ( x = [2,<*(s . 1),(s . 2),(s . 3)*>] & y = [0,<*(s . 1),(s . 3)*>] ) ) by A26, A27, A29, MCART_1:21; :: thesis:

end;

consider R being Function such that
A32: ( dom R = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & rng R c= [:{0},(2 -tuples_on A):] ) and
A33: for x being object st x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] holds
S₁[x,R . x] from FUNCT_1:sch 6(A19);
reconsider R = R as Function of ([:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):]),[:{0},(2 -tuples_on A):] by A32, FUNCT_2:2;
take S = ManySortedSign(# [:{0},(2 -tuples_on A):],([:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):]),Ar,R #); :: thesis:
thus the carrier of S = [:{0},(2 -tuples_on A):] ; :: thesis:
thus the carrier' of S = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; :: thesis:

hereby :: thesis:

let a be set ; :: thesis:
assume A34: a in A ; :: thesis:
then reconsider B = A as non empty set ;
reconsider x = a as Element of B by A34;
( <*x*> is Element of 1 -tuples_on B & 1 in {1} ) by FINSEQ_2:98, TARSKI:def 1;
then [1,<*a*>] in [:{1},(1 -tuples_on A):] by ZFMISC_1:87;
then A35: [1,<*a*>] in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by XBOOLE_0:def 3;
then consider y1, y2, y3 being set such that
y1 in A and
y2 in A and
y3 in A and
A36: ( ( [1,<*a*>] = [1,<*y1*>] & R . [1,<*a*>] = [0,<*y1,y1*>] ) or ( [1,<*a*>] = [2,<*y1,y2,y3*>] & R . [1,<*a*>] = [0,<*y1,y3*>] ) ) by A33;
ex y1, y2, y3 being set st
( y1 in A & y2 in A & y3 in A & ( ( [1,<*a*>] = [1,<*y1*>] & Ar . [1,<*a*>] = {} ) or ( [1,<*a*>] = [2,<*y1,y2,y3*>] & Ar . [1,<*a*>] = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) ) by A18, A35;
hence the Arity of S . [1,<*a*>] = {} by XTUPLE_0:1; :: thesis:
A37: ( <*a*> . 1 = a & <*y1*> . 1 = y1 ) ;
<*a*> = <*y1*> by A36, XTUPLE_0:1;
hence the ResultSort of S . [1,<*a*>] = [0,<*a,a*>] by A36, A37, XTUPLE_0:1; :: thesis:

end;

let a, b, c be set ; :: thesis:
assume that
A38: a in A and
A39: ( b in A & c in A ) ; :: thesis:
reconsider B = A as non empty set by A38;
reconsider x = a, y = b, z = c as Element of B by A38, A39;
( <*x,y,z*> is Element of 3 -tuples_on B & 2 in {2} ) by FINSEQ_2:104, TARSKI:def 1;
then [2,<*a,b,c*>] in [:{2},(3 -tuples_on A):] by ZFMISC_1:87;
then A40: [2,<*a,b,c*>] in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by XBOOLE_0:def 3;
then consider y1, y2, y3 being set such that
y1 in A and
y2 in A and
y3 in A and
A41: ( ( [2,<*a,b,c*>] = [1,<*y1*>] & Ar . [2,<*a,b,c*>] = {} ) or ( [2,<*a,b,c*>] = [2,<*y1,y2,y3*>] & Ar . [2,<*a,b,c*>] = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) by A18;
A42: ( <*a,b,c*> = (<*a*> ^ <*b*>) ^ <*c*> & <*y1,y2,y3*> = (<*y1*> ^ <*y2*>) ^ <*y3*> ) by FINSEQ_1:def 10;
A43: <*a,b,c*> = <*y1,y2,y3*> by A41, XTUPLE_0:1;
then A44: <*a*> ^ <*b*> = <*y1*> ^ <*y2*> by A42, FINSEQ_2:17;
then <*a*> = <*y1*> by FINSEQ_2:17;
then A45: a = y1 by Lm1;
b = y2 by A44, FINSEQ_2:17;
hence the Arity of S . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> by A41, A43, A42, A45, FINSEQ_2:17, XTUPLE_0:1; :: thesis:
consider y1, y2, y3 being set such that
y1 in A and
y2 in A and
y3 in A and
A46: ( ( [2,<*a,b,c*>] = [1,<*y1*>] & R . [2,<*a,b,c*>] = [0,<*y1,y1*>] ) or ( [2,<*a,b,c*>] = [2,<*y1,y2,y3*>] & R . [2,<*a,b,c*>] = [0,<*y1,y3*>] ) ) by A33, A40;
A47: ( <*a,b,c*> . 1 = a & <*y1,y2,y3*> . 1 = y1 ) ;
A48: <*a,b,c*> . 3 = c ;
<*a,b,c*> = <*y1,y2,y3*> by A46, XTUPLE_0:1;
hence the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] by A46, A47, A48, FINSEQ_1:45, XTUPLE_0:1; :: thesis: