defpred S₁[ set , set ] 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 set st x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] holds
ex y being set st
( y in [:{0 },(2 -tuples_on A):] * & S₁[x,y] )

proof

let x be set ; :: 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 `1 in {1} & x `2 in 1 -tuples_on A ) by MCART_1:10;
then A4: ( x `1 = 1 & x `2 in { s where s is Element of A * : len s = 1 } ) by FINSEQ_2:def 4, TARSKI:def 1;
then consider s being Element of A * such that
A5: ( x `2 = s & len s = 1 ) ;
take y = {} ; :: thesis:
thus y in [:{0 },(2 -tuples_on A):] * by FINSEQ_1:66; :: thesis:
take y1 = s . 1; :: thesis:
take y2 = s . 1; :: thesis:
take y3 = s . 1; :: thesis:
A6: s = <*y1*> by A5, FINSEQ_1:57;
then ( y1 in {y1} & rng s = {y1} & rng s c= A ) by FINSEQ_1:56, TARSKI:def 1;
hence ( y1 in A & y2 in A & y3 in A ) ; :: thesis:
thus ( ( x = [1,<*y1*>] & y = {} ) or ( x = [2,<*y1,y2,y3*>] & y = <*[0 ,<*y2,y3*>],[0 ,<*y1,y2*>]*> ) ) by A3, A4, A5, A6, MCART_1:23; :: thesis:

end;

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

then ( x `1 in {2} & x `2 in 3 -tuples_on A ) by MCART_1:10;
then A8: ( x `1 = 2 & x `2 in { s where s is Element of A * : len s = 3 } ) by FINSEQ_2:def 4, TARSKI:def 1;
then consider s being Element of A * such that
A9: ( x `2 = s & len s = 3 ) ;
set y1 = s . 1;
set y2 = s . 2;
set y3 = s . 3;
A10: s = <*(s . 1),(s . 2),(s . 3)*> by A9, FINSEQ_1:62;
then A11: ( s . 1 in {(s . 1),(s . 2),(s . 3)} & s . 2 in {(s . 1),(s . 2),(s . 3)} & s . 3 in {(s . 1),(s . 2),(s . 3)} & rng s = {(s . 1),(s . 2),(s . 3)} & rng s c= A ) by ENUMSET1:def 1, FINSEQ_2:148;
then reconsider B = A as non empty set ;
take y = <*[0 ,<*(s . 2),(s . 3)*>],[0 ,<*(s . 1),(s . 2)*>]*>; :: thesis:
( <*(s . 2),(s . 3)*> is Element of 2 -tuples_on B & <*(s . 1),(s . 2)*> is Element of 2 -tuples_on B ) by A11, FINSEQ_2:121;
then ( <*(s . 2),(s . 3)*> in 2 -tuples_on B & 0 in {0 } & <*(s . 1),(s . 2)*> in 2 -tuples_on B ) by TARSKI:def 1;
then reconsider z1 = [0 ,<*(s . 2),(s . 3)*>], z2 = [0 ,<*(s . 1),(s . 2)*>] as Element of [:{0 },(2 -tuples_on B):] by ZFMISC_1:106;
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 A11; :: thesis:
thus ( ( 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 A7, A8, A9, A10, MCART_1:23; :: thesis:

end;

consider Ar being Function such that
A12: dom Ar = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] and
A13: rng Ar c= [:{0 },(2 -tuples_on A):] * and
A14: for x being set st x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] holds
S₁[x,Ar . x] from WELLORD2:sch 1(A1);
reconsider Ar = Ar as Function of ([:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):]),([:{0 },(2 -tuples_on A):] * ) by A12, A13, FUNCT_2:4;
defpred S₂[ set , set ] 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*>] ) ) );
A15: for x being set st x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] holds
ex y being set st
( y in [:{0 },(2 -tuples_on A):] & S₂[x,y] )

proof

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

per cases by A16, XBOOLE_0:def 3;

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

then ( x `1 in {1} & x `2 in 1 -tuples_on A ) by MCART_1:10;
then A18: ( x `1 = 1 & x `2 in { s where s is Element of A * : len s = 1 } ) by FINSEQ_2:def 4, TARSKI:def 1;
then consider s being Element of A * such that
A19: ( x `2 = s & len s = 1 ) ;
set y1 = s . 1;
set y2 = s . 1;
set y3 = s . 1;
take y = [0 ,<*(s . 1),(s . 1)*>]; :: thesis:
A20: s = <*(s . 1)*> by A19, FINSEQ_1:57;
then A21: ( s . 1 in {(s . 1)} & rng s = {(s . 1)} & rng s c= A ) by FINSEQ_1:56, TARSKI:def 1;
then reconsider B = A as non empty set ;
reconsider y1 = s . 1 as Element of B by A21;
<*y1,y1*> is Element of 2 -tuples_on B by FINSEQ_2:121;
then ( 0 in {0 } & <*y1,y1*> in 2 -tuples_on B ) by TARSKI:def 1;
hence y in [:{0 },(2 -tuples_on A):] by ZFMISC_1:106; :: 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 A21; :: thesis:
thus ( ( x = [1,<*y1*>] & y = [0 ,<*y1,y1*>] ) or ( x = [2,<*y1,(s . 1),(s . 1)*>] & y = [0 ,<*y1,(s . 1)*>] ) ) by A17, A18, A19, A20, MCART_1:23; :: thesis:

end;

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

then ( x `1 in {2} & x `2 in 3 -tuples_on A ) by MCART_1:10;
then A23: ( x `1 = 2 & x `2 in { s where s is Element of A * : len s = 3 } ) by FINSEQ_2:def 4, TARSKI:def 1;
then consider s being Element of A * such that
A24: ( x `2 = s & len s = 3 ) ;
set y1 = s . 1;
set y2 = s . 2;
set y3 = s . 3;
A25: s = <*(s . 1),(s . 2),(s . 3)*> by A24, FINSEQ_1:62;
then A26: ( s . 1 in {(s . 1),(s . 2),(s . 3)} & s . 2 in {(s . 1),(s . 2),(s . 3)} & s . 3 in {(s . 1),(s . 2),(s . 3)} & rng s = {(s . 1),(s . 2),(s . 3)} & rng s c= A ) by ENUMSET1:def 1, FINSEQ_2:148;
then reconsider B = A as non empty set ;
take y = [0 ,<*(s . 1),(s . 3)*>]; :: thesis:
<*(s . 1),(s . 3)*> is Element of 2 -tuples_on B by A26, FINSEQ_2:121;
then ( 0 in {0 } & <*(s . 1),(s . 3)*> in 2 -tuples_on B ) by TARSKI:def 1;
hence y in [:{0 },(2 -tuples_on A):] by ZFMISC_1:106; :: 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 A26; :: thesis:
thus ( ( 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 A22, A23, A24, A25, MCART_1:23; :: thesis:

end;

consider R being Function such that
A27: dom R = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] and
A28: rng R c= [:{0 },(2 -tuples_on A):] and
A29: for x being set st x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] holds
S₂[x,R . x] from WELLORD2:sch 1(A15);
reconsider R = R as Function of ([:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):]),[:{0 },(2 -tuples_on A):] by A27, A28, FUNCT_2:4;
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 A30: a in A ; :: thesis:
then reconsider B = A as non empty set ;
reconsider x = a as Element of B by A30;
( <*x*> is Element of 1 -tuples_on B & 1 in {1} ) by FINSEQ_2:118, TARSKI:def 1;
then [1,<*a*>] in [:{1},(1 -tuples_on A):] by ZFMISC_1:106;
then A31: [1,<*a*>] in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by XBOOLE_0:def 3;
then ( 1 <> 2 & 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 A14;
hence the Arity of S . [1,<*a*>] = {} by ZFMISC_1:33; :: thesis:
consider y1, y2, y3 being set such that
( y1 in A & y2 in A & y3 in A ) and
A32: ( ( [1,<*a*>] = [1,<*y1*>] & R . [1,<*a*>] = [0 ,<*y1,y1*>] ) or ( [1,<*a*>] = [2,<*y1,y2,y3*>] & R . [1,<*a*>] = [0 ,<*y1,y3*>] ) ) by A29, A31;
( <*a*> = <*y1*> & R . [1,<*a*>] = [0 ,<*y1,y1*>] & <*a*> . 1 = a & <*y1*> . 1 = y1 ) by A32, FINSEQ_1:57, ZFMISC_1:33;
hence the ResultSort of S . [1,<*a*>] = [0 ,<*a,a*>] ; :: thesis:

end;

let a, b, c be set ; :: thesis:
assume A33: ( a in A & b in A & c in A ) ; :: thesis:
then reconsider B = A as non empty set ;
reconsider x = a, y = b, z = c as Element of B by A33;
( <*x,y,z*> is Element of 3 -tuples_on B & 2 in {2} ) by FINSEQ_2:124, TARSKI:def 1;
then [2,<*a,b,c*>] in [:{2},(3 -tuples_on A):] by ZFMISC_1:106;
then A34: [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 & y2 in A & y3 in A ) and
A35: ( ( [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 A14;
A36: ( <*a,b,c*> = <*y1,y2,y3*> & Ar . [2,<*a,b,c*>] = <*[0 ,<*y2,y3*>],[0 ,<*y1,y2*>]*> ) by A35, ZFMISC_1:33;
A37: ( <*a,b,c*> = (<*a*> ^ <*b*>) ^ <*c*> & <*y1,y2,y3*> = (<*y1*> ^ <*y2*>) ^ <*y3*> ) by FINSEQ_1:def 10;
then ( <*a*> ^ <*b*> = <*y1*> ^ <*y2*> & <*y3*> = <*c*> ) by A36, FINSEQ_2:20;
then ( <*a*> = <*y1*> & <*y2*> = <*b*> ) by FINSEQ_2:20;
then ( a = y1 & b = y2 & c = y3 ) by A36, A37, Lm1, FINSEQ_2:20;
hence the Arity of S . [2,<*a,b,c*>] = <*[0 ,<*b,c*>],[0 ,<*a,b*>]*> by A35, ZFMISC_1:33; :: thesis:
consider y1, y2, y3 being set such that
( y1 in A & y2 in A & y3 in A ) and
A38: ( ( [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 A29, A34;
( <*a,b,c*> = <*y1,y2,y3*> & R . [2,<*a,b,c*>] = [0 ,<*y1,y3*>] & <*a,b,c*> . 1 = a & <*y1,y2,y3*> . 1 = y1 & <*a,b,c*> . 3 = c & <*y1,y2,y3*> . 3 = y3 ) by A38, FINSEQ_1:62, ZFMISC_1:33;
hence the ResultSort of S . [2,<*a,b,c*>] = [0 ,<*a,c*>] ; :: thesis: