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 ;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;
then rng () c= dom the Sorts of U1 ;
then A4: dom ( the Sorts of U1 * ()) = dom () by RELAT_1:27;
A5: dom ( the Sorts of U2 * ()) c= dom () 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 #) . () by MSUALG_1:def 1 ;
then product ( the Sorts of U1 * ()) <> {} by ;
then A7: not {} in rng ( the Sorts of U1 * ()) by CARD_3:26;
now :: thesis: for x being object st x in dom ( the Sorts of U2 * ()) holds
( the Sorts of U2 * ()) . x <> {}
let x be object ; :: thesis: ( x in dom ( the Sorts of U2 * ()) implies ( the Sorts of U2 * ()) . x <> {} )
assume A8: x in dom ( the Sorts of U2 * ()) ; :: thesis: ( the Sorts of U2 * ()) . x <> {}
then (the_arity_of o) . x in rng () by ;
then A9: ( the Sorts of U1 . (() . x) <> {} implies the Sorts of U2 . (() . x) <> {} ) by ;
( the Sorts of U1 * ()) . x = the Sorts of U1 . (() . x) by ;
hence ( the Sorts of U2 * ()) . x <> {} by ; :: thesis: verum
end;
then not {} in rng ( the Sorts of U2 * ()) by FUNCT_1:def 3;
then product ( the Sorts of U2 * ()) <> {} by CARD_3:26;
then ( the Sorts of U2 #) . () <> {} 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 ;
hence Args (o,U2) <> {} by MSUALG_1:def 4; :: thesis: verum