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
A49: the carrier of S1 = [:{0},(2 -tuples_on A):] and
A50: the carrier' of S1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] and
A51: 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
A52: 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
A53: the carrier of S2 = [:{0},(2 -tuples_on A):] and
A54: the carrier' of S2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] and
A55: 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
A56: 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

A57: now :: thesis: for x being object st x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] holds
the Arity of S1 . x = the Arity of S2 . x

let x be object ; :: 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 A58: ( x in [:{1},(1 -tuples_on A):] or x in [:{2},(3 -tuples_on A):] ) by XBOOLE_0:def 3;
then ( ( 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;
then A59: ( ( 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;

A60: now :: thesis: ( x `2 in 3 -tuples_on A implies the Arity of S1 . [2,(x `2)] = the Arity of S2 . [2,(x `2)] )

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 object such that
A61: ( a in A & b in A & c in A & x `2 = <*a,b,c*> ) by FINSEQ_2:139;
thus the Arity of S1 . [2,(x `2)] = <*[0,<*b,c*>],[0,<*a,b*>]*> by A52, A61
.= the Arity of S2 . [2,(x `2)] by A56, A61 ; :: thesis: verum

end;

A62: now :: thesis: ( x `2 in 1 -tuples_on A implies the Arity of S1 . [1,(x `2)] = the Arity of S2 . [1,(x `2)] )

assume x `2 in 1 -tuples_on A ; :: thesis: the Arity of S1 . [1,(x `2)] = the Arity of S2 . [1,(x `2)]
then A63: ex a being set st
( a in A & x `2 = <*a*> ) by FINSEQ_2:135;
hence the Arity of S1 . [1,(x `2)] = {} by A51
.= the Arity of S2 . [1,(x `2)] by A55, A63 ;
:: thesis: verum

end;

x = [(x `1),(x `2)] by A58, MCART_1:21;
hence the Arity of S1 . x = the Arity of S2 . x by A59, A62, A60; :: thesis: verum

end;

A64: now :: thesis: for x being object st x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] holds
the ResultSort of S1 . x = the ResultSort of S2 . x

let x be object ; :: 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 A65: ( x in [:{1},(1 -tuples_on A):] or x in [:{2},(3 -tuples_on A):] ) by XBOOLE_0:def 3;
then ( ( 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;
then A66: ( ( 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;

A67: now :: thesis: ( x `2 in 3 -tuples_on A implies the ResultSort of S1 . [2,(x `2)] = the ResultSort of S2 . [2,(x `2)] )

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 object such that
A68: ( a in A & b in A & c in A & x `2 = <*a,b,c*> ) by FINSEQ_2:139;
thus the ResultSort of S1 . [2,(x `2)] = [0,<*a,c*>] by A52, A68
.= the ResultSort of S2 . [2,(x `2)] by A56, A68 ; :: thesis: verum

end;

A69: now :: thesis: ( x `2 in 1 -tuples_on A implies the ResultSort of S1 . [1,(x `2)] = the ResultSort of S2 . [1,(x `2)] )

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
A70: ( a in A & x `2 = <*a*> ) by FINSEQ_2:135;
thus the ResultSort of S1 . [1,(x `2)] = [0,<*a,a*>] by A51, A70
.= the ResultSort of S2 . [1,(x `2)] by A55, A70 ; :: thesis: verum

end;

x = [(x `1),(x `2)] by A65, MCART_1:21;
hence the ResultSort of S1 . x = the ResultSort of S2 . x by A66, A69, A67; :: thesis: verum

end;

( dom the Arity of S1 = the carrier' of S1 & dom the Arity of S2 = the carrier' of S2 ) by FUNCT_2:def 1;
then A71: the Arity of S1 = the Arity of S2 by A50, A54, A57, FUNCT_1:2;

now :: thesis: ( [:{0},(2 -tuples_on A):] = {} implies [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] = {} )

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

end;

then ( dom the ResultSort of S1 = the carrier' of S1 & dom the ResultSort of S2 = the carrier' of S2 ) by A49, A50, A53, A54, FUNCT_2:def 1;
hence S1 = S2 by A49, A50, A53, A54, A71, A64, FUNCT_1:2; :: thesis: verum