let S be non empty non void ManySortedSign ; :: thesis: for A1, A2 being MSAlgebra of 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 of 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

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