let S1, S2 be strict ManySortedSign ; :: thesis: ( the carrier of S1 = [:{0 },(2 -tuples_on A):] & the carrier' of S1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of S1 . [1,<*a*>] = {} & the ResultSort of S1 . [1,<*a*>] = [0 ,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds
( the Arity of S1 . [2,<*a,b,c*>] = <*[0 ,<*b,c*>],[0 ,<*a,b*>]*> & the ResultSort of S1 . [2,<*a,b,c*>] = [0 ,<*a,c*>] ) ) & the carrier of S2 = [:{0 },(2 -tuples_on A):] & the carrier' of S2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of S2 . [1,<*a*>] = {} & the ResultSort of S2 . [1,<*a*>] = [0 ,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds
( the Arity of S2 . [2,<*a,b,c*>] = <*[0 ,<*b,c*>],[0 ,<*a,b*>]*> & the ResultSort of S2 . [2,<*a,b,c*>] = [0 ,<*a,c*>] ) ) implies S1 = S2 )
assume that
A39: the carrier of S1 = [:{0 },(2 -tuples_on A):] and
A40: the carrier' of S1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] and
A41: for a being set st a in A holds
( the Arity of S1 . [1,<*a*>] = {} & the ResultSort of S1 . [1,<*a*>] = [0 ,<*a,a*>] ) and
A42: for a, b, c being set st a in A & b in A & c in A holds
( the Arity of S1 . [2,<*a,b,c*>] = <*[0 ,<*b,c*>],[0 ,<*a,b*>]*> & the ResultSort of S1 . [2,<*a,b,c*>] = [0 ,<*a,c*>] ) and
A43: the carrier of S2 = [:{0 },(2 -tuples_on A):] and
A44: the carrier' of S2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] and
A45: for a being set st a in A holds
( the Arity of S2 . [1,<*a*>] = {} & the ResultSort of S2 . [1,<*a*>] = [0 ,<*a,a*>] ) and
A46: for a, b, c being set st a in A & b in A & c in A holds
( the Arity of S2 . [2,<*a,b,c*>] = <*[0 ,<*b,c*>],[0 ,<*a,b*>]*> & the ResultSort of S2 . [2,<*a,b,c*>] = [0 ,<*a,c*>] ) ; :: thesis: S1 = S2
A47: ( dom the Arity of S1 = the carrier' of S1 & dom the Arity of S2 = the carrier' of S2 ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] implies the Arity of S1 . x = the Arity of S2 . x )
assume x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; :: thesis: the Arity of S1 . x = the Arity of S2 . x
then ( x in [:{1},(1 -tuples_on A):] or x in [:{2},(3 -tuples_on A):] ) by XBOOLE_0:def 3;
then A48: ( x = [(x `1 ),(x `2 )] & ( ( x `1 in {1} & x `2 in 1 -tuples_on A ) or ( x `1 in {2} & x `2 in 3 -tuples_on A ) ) ) by MCART_1:10, MCART_1:23;
then A49: ( ( x `1 = 1 & x `2 in 1 -tuples_on A ) or ( x `1 = 2 & x `2 in 3 -tuples_on A ) ) by TARSKI:def 1;

A50: now

assume x `2 in 1 -tuples_on A ; :: thesis: the Arity of S1 . [1,(x `2 )] = the Arity of S2 . [1,(x `2 )]
then consider a being set such that
A51: ( a in A & x `2 = <*a*> ) by Th8;
thus the Arity of S1 . [1,(x `2 )] = {} by A41, A51
.= the Arity of S2 . [1,(x `2 )] by A45, A51 ; :: thesis: verum

end;

now

assume x `2 in 3 -tuples_on A ; :: thesis: the Arity of S1 . [2,(x `2 )] = the Arity of S2 . [2,(x `2 )]
then consider a, b, c being set such that
A52: ( a in A & b in A & c in A & x `2 = <*a,b,c*> ) by Th12;
thus the Arity of S1 . [2,(x `2 )] = <*[0 ,<*b,c*>],[0 ,<*a,b*>]*> by A42, A52
.= the Arity of S2 . [2,(x `2 )] by A46, A52 ; :: thesis: verum

end;

hence the Arity of S1 . x = the Arity of S2 . x by A48, A49, A50; :: thesis: verum

end;

then A53: the Arity of S1 = the Arity of S2 by A40, A44, A47, FUNCT_1:9;

now

assume A54: [:{0 },(2 -tuples_on A):] = {} ; :: thesis: [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] = {}
A = {} by A54;
then ( 1 <> 0 & 3 <> 0 implies ( 1 -tuples_on A = {} & 3 -tuples_on A = {} ) ) by Th7;
then ( [:{1},(1 -tuples_on A):] = {} & [:{2},(3 -tuples_on A):] = {} ) by ZFMISC_1:113;
hence [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] = {} ; :: thesis: verum

end;

then A55: ( dom the ResultSort of S1 = the carrier' of S1 & dom the ResultSort of S2 = the carrier' of S2 ) by A39, A40, A43, A44, FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] implies the ResultSort of S1 . x = the ResultSort of S2 . x )
assume x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; :: thesis: the ResultSort of S1 . x = the ResultSort of S2 . x
then ( x in [:{1},(1 -tuples_on A):] or x in [:{2},(3 -tuples_on A):] ) by XBOOLE_0:def 3;
then A56: ( x = [(x `1 ),(x `2 )] & ( ( x `1 in {1} & x `2 in 1 -tuples_on A ) or ( x `1 in {2} & x `2 in 3 -tuples_on A ) ) ) by MCART_1:10, MCART_1:23;
then A57: ( ( x `1 = 1 & x `2 in 1 -tuples_on A ) or ( x `1 = 2 & x `2 in 3 -tuples_on A ) ) by TARSKI:def 1;

A58: now

assume x `2 in 1 -tuples_on A ; :: thesis: the ResultSort of S1 . [1,(x `2 )] = the ResultSort of S2 . [1,(x `2 )]
then consider a being set such that
A59: ( a in A & x `2 = <*a*> ) by Th8;
thus the ResultSort of S1 . [1,(x `2 )] = [0 ,<*a,a*>] by A41, A59
.= the ResultSort of S2 . [1,(x `2 )] by A45, A59 ; :: thesis: verum

end;

now

assume x `2 in 3 -tuples_on A ; :: thesis: the ResultSort of S1 . [2,(x `2 )] = the ResultSort of S2 . [2,(x `2 )]
then consider a, b, c being set such that
A60: ( a in A & b in A & c in A & x `2 = <*a,b,c*> ) by Th12;
thus the ResultSort of S1 . [2,(x `2 )] = [0 ,<*a,c*>] by A42, A60
.= the ResultSort of S2 . [2,(x `2 )] by A46, A60 ; :: thesis: verum

end;

hence the ResultSort of S1 . x = the ResultSort of S2 . x by A56, A57, A58; :: thesis: verum

end;

hence S1 = S2 by A39, A40, A43, A44, A53, A55, FUNCT_1:9; :: thesis: verum