let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S

for U1, U2 being MSAlgebra over S st the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} holds

Args (o,U2) <> {}

let o be OperSymbol of S; :: thesis: for U1, U2 being MSAlgebra over S st the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} holds

Args (o,U2) <> {}

let U1, U2 be MSAlgebra over S; :: thesis: ( the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} implies Args (o,U2) <> {} )

assume that

A1: the Sorts of U1 is_transformable_to the Sorts of U2 and

A2: Args (o,U1) <> {} ; :: thesis: Args (o,U2) <> {}

A3: (( the Sorts of U1 #) * the Arity of S) . o <> {} by A2, MSUALG_1:def 4;

dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;

then rng (the_arity_of o) c= dom the Sorts of U1 ;

then A4: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;

A5: dom ( the Sorts of U2 * (the_arity_of o)) c= dom (the_arity_of o) by RELAT_1:25;

A6: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;

then (( the Sorts of U1 #) * the Arity of S) . o = ( the Sorts of U1 #) . ( the Arity of S . o) by FUNCT_1:13

.= ( the Sorts of U1 #) . (the_arity_of o) by MSUALG_1:def 1 ;

then product ( the Sorts of U1 * (the_arity_of o)) <> {} by A3, FINSEQ_2:def 5;

then A7: not {} in rng ( the Sorts of U1 * (the_arity_of o)) by CARD_3:26;

then product ( the Sorts of U2 * (the_arity_of o)) <> {} by CARD_3:26;

then ( the Sorts of U2 #) . (the_arity_of o) <> {} by FINSEQ_2:def 5;

then ( the Sorts of U2 #) . ( the Arity of S . o) <> {} by MSUALG_1:def 1;

then (( the Sorts of U2 #) * the Arity of S) . o <> {} by A6, FUNCT_1:13;

hence Args (o,U2) <> {} by MSUALG_1:def 4; :: thesis: verum

for U1, U2 being MSAlgebra over S st the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} holds

Args (o,U2) <> {}

let o be OperSymbol of S; :: thesis: for U1, U2 being MSAlgebra over S st the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} holds

Args (o,U2) <> {}

let U1, U2 be MSAlgebra over S; :: thesis: ( the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} implies Args (o,U2) <> {} )

assume that

A1: the Sorts of U1 is_transformable_to the Sorts of U2 and

A2: Args (o,U1) <> {} ; :: thesis: Args (o,U2) <> {}

A3: (( the Sorts of U1 #) * the Arity of S) . o <> {} by A2, MSUALG_1:def 4;

dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;

then rng (the_arity_of o) c= dom the Sorts of U1 ;

then A4: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;

A5: dom ( the Sorts of U2 * (the_arity_of o)) c= dom (the_arity_of o) by RELAT_1:25;

A6: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;

then (( the Sorts of U1 #) * the Arity of S) . o = ( the Sorts of U1 #) . ( the Arity of S . o) by FUNCT_1:13

.= ( the Sorts of U1 #) . (the_arity_of o) by MSUALG_1:def 1 ;

then product ( the Sorts of U1 * (the_arity_of o)) <> {} by A3, FINSEQ_2:def 5;

then A7: not {} in rng ( the Sorts of U1 * (the_arity_of o)) by CARD_3:26;

now :: thesis: for x being object st x in dom ( the Sorts of U2 * (the_arity_of o)) holds

( the Sorts of U2 * (the_arity_of o)) . x <> {}

then
not {} in rng ( the Sorts of U2 * (the_arity_of o))
by FUNCT_1:def 3;( the Sorts of U2 * (the_arity_of o)) . x <> {}

let x be object ; :: thesis: ( x in dom ( the Sorts of U2 * (the_arity_of o)) implies ( the Sorts of U2 * (the_arity_of o)) . x <> {} )

assume A8: x in dom ( the Sorts of U2 * (the_arity_of o)) ; :: thesis: ( the Sorts of U2 * (the_arity_of o)) . x <> {}

then (the_arity_of o) . x in rng (the_arity_of o) by A5, FUNCT_1:def 3;

then A9: ( the Sorts of U1 . ((the_arity_of o) . x) <> {} implies the Sorts of U2 . ((the_arity_of o) . x) <> {} ) by A1, PZFMISC1:def 3;

( the Sorts of U1 * (the_arity_of o)) . x = the Sorts of U1 . ((the_arity_of o) . x) by A5, A8, FUNCT_1:13;

hence ( the Sorts of U2 * (the_arity_of o)) . x <> {} by A7, A4, A5, A8, A9, FUNCT_1:13, FUNCT_1:def 3; :: thesis: verum

end;assume A8: x in dom ( the Sorts of U2 * (the_arity_of o)) ; :: thesis: ( the Sorts of U2 * (the_arity_of o)) . x <> {}

then (the_arity_of o) . x in rng (the_arity_of o) by A5, FUNCT_1:def 3;

then A9: ( the Sorts of U1 . ((the_arity_of o) . x) <> {} implies the Sorts of U2 . ((the_arity_of o) . x) <> {} ) by A1, PZFMISC1:def 3;

( the Sorts of U1 * (the_arity_of o)) . x = the Sorts of U1 . ((the_arity_of o) . x) by A5, A8, FUNCT_1:13;

hence ( the Sorts of U2 * (the_arity_of o)) . x <> {} by A7, A4, A5, A8, A9, FUNCT_1:13, FUNCT_1:def 3; :: thesis: verum

then product ( the Sorts of U2 * (the_arity_of o)) <> {} by CARD_3:26;

then ( the Sorts of U2 #) . (the_arity_of o) <> {} by FINSEQ_2:def 5;

then ( the Sorts of U2 #) . ( the Arity of S . o) <> {} by MSUALG_1:def 1;

then (( the Sorts of U2 #) * the Arity of S) . o <> {} by A6, FUNCT_1:13;

hence Args (o,U2) <> {} by MSUALG_1:def 4; :: thesis: verum