let S be non empty non void ManySortedSign ; :: thesis: for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for o being OperSymbol of S st Args (o,A1) <> {} holds
Args (o,A2) <> {}
let A1, A2 be MSAlgebra over S; :: thesis: ( the Sorts of A1 is_transformable_to the Sorts of A2 implies for o being OperSymbol of S st Args (o,A1) <> {} holds
Args (o,A2) <> {} )
assume A1: for i being set st i in the carrier of S & the Sorts of A2 . i = {} holds
the Sorts of A1 . i = {} ; :: according to PZFMISC1:def 3 :: thesis: for o being OperSymbol of S st Args (o,A1) <> {} holds
Args (o,A2) <> {}
let o be OperSymbol of S; :: thesis: ( Args (o,A1) <> {} implies Args (o,A2) <> {} )
assume A2: Args (o,A1) <> {} ; :: thesis: Args (o,A2) <> {}

now :: thesis: for i being Element of NAT st i in dom (the_arity_of o) holds
the Sorts of A2 . ((the_arity_of o) /. i) <> {}

let i be Element of NAT ; :: thesis: ( i in dom (the_arity_of o) implies the Sorts of A2 . ((the_arity_of o) /. i) <> {} )
assume i in dom (the_arity_of o) ; :: thesis: the Sorts of A2 . ((the_arity_of o) /. i) <> {}
then the Sorts of A1 . ((the_arity_of o) /. i) <> {} by A2, MSUALG_6:3;
hence the Sorts of A2 . ((the_arity_of o) /. i) <> {} by A1; :: thesis: verum

end;

hence Args (o,A2) <> {} by MSUALG_6:3; :: thesis: verum