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) <> {}

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) <> {}

hence
Args (o,A2) <> {}
by MSUALG_6:3; :: thesis: verumthe 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;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