let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U1, U2 being MSAlgebra of 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 of 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 of 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 9;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def 4;
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:46;
A5: dom (the Sorts of U2 * (the_arity_of o)) c= dom (the_arity_of o) by RELAT_1:44;
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:23
.= (the Sorts of U1 # ) . (the_arity_of o) by MSUALG_1:def 6 ;
then product (the Sorts of U1 * (the_arity_of o)) <> {} by A3, PBOOLE:def 19;
then A7: not {} in rng (the Sorts of U1 * (the_arity_of o)) by CARD_3:37;

now

let x be set ; :: 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 5;
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:23;
hence (the Sorts of U2 * (the_arity_of o)) . x <> {} by A7, A4, A5, A8, A9, FUNCT_1:23, FUNCT_1:def 5; :: thesis: verum

end;

then not {} in rng (the Sorts of U2 * (the_arity_of o)) by FUNCT_1:def 5;
then product (the Sorts of U2 * (the_arity_of o)) <> {} by CARD_3:37;
then (the Sorts of U2 # ) . (the_arity_of o) <> {} by PBOOLE:def 19;
then (the Sorts of U2 # ) . (the Arity of S . o) <> {} by MSUALG_1:def 6;
then ((the Sorts of U2 # ) * the Arity of S) . o <> {} by A6, FUNCT_1:23;
hence Args o,U2 <> {} by MSUALG_1:def 9; :: thesis: verum