let S1 be feasible ManySortedSign ; :: thesis: for S2 being Subsignature of S1 st S1 is Subsignature of S2 holds

ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #)

let S2 be Subsignature of S1; :: thesis: ( S1 is Subsignature of S2 implies ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) )

A1: the carrier of S2 c= the carrier of S1 by Th10;

assume A2: S1 is Subsignature of S2 ; :: thesis: ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #)

then the carrier of S1 c= the carrier of S2 by Th10;

then A3: the carrier of S1 = the carrier of S2 by A1, XBOOLE_0:def 10;

A4: the carrier' of S2 c= the carrier' of S1 by Th10;

the carrier' of S1 c= the carrier' of S2 by A2, Th10;

then A5: the carrier' of S1 = the carrier' of S2 by A4, XBOOLE_0:def 10;

A6: the Arity of S2 c= the Arity of S1 by Th11;

A7: the ResultSort of S2 c= the ResultSort of S1 by Th11;

the ResultSort of S1 c= the ResultSort of S2 by A2, Th11;

then A8: the ResultSort of S1 = the ResultSort of S2 by A7, XBOOLE_0:def 10;

the Arity of S1 c= the Arity of S2 by A2, Th11;

hence ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) by A6, A3, A5, A8, XBOOLE_0:def 10; :: thesis: verum

ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #)

let S2 be Subsignature of S1; :: thesis: ( S1 is Subsignature of S2 implies ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) )

A1: the carrier of S2 c= the carrier of S1 by Th10;

assume A2: S1 is Subsignature of S2 ; :: thesis: ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #)

then the carrier of S1 c= the carrier of S2 by Th10;

then A3: the carrier of S1 = the carrier of S2 by A1, XBOOLE_0:def 10;

A4: the carrier' of S2 c= the carrier' of S1 by Th10;

the carrier' of S1 c= the carrier' of S2 by A2, Th10;

then A5: the carrier' of S1 = the carrier' of S2 by A4, XBOOLE_0:def 10;

A6: the Arity of S2 c= the Arity of S1 by Th11;

A7: the ResultSort of S2 c= the ResultSort of S1 by Th11;

the ResultSort of S1 c= the ResultSort of S2 by A2, Th11;

then A8: the ResultSort of S1 = the ResultSort of S2 by A7, XBOOLE_0:def 10;

the Arity of S1 c= the Arity of S2 by A2, Th11;

hence ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) by A6, A3, A5, A8, XBOOLE_0:def 10; :: thesis: verum