let S be non empty non void ManySortedSign ; :: thesis: for A1, A2 being MSAlgebra of S
for h being ManySortedFunction of A1,A2
for o being OperSymbol of S st Args o,A1 <> {} & Args o,A2 <> {} holds
for i being Element of NAT st i in dom (the_arity_of o) holds
for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i)
let A1, A2 be MSAlgebra of S; :: thesis: for h being ManySortedFunction of A1,A2
for o being OperSymbol of S st Args o,A1 <> {} & Args o,A2 <> {} holds
for i being Element of NAT st i in dom (the_arity_of o) holds
for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i)
let h be ManySortedFunction of A1,A2; :: thesis: for o being OperSymbol of S st Args o,A1 <> {} & Args o,A2 <> {} holds
for i being Element of NAT st i in dom (the_arity_of o) holds
for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i)
let o be OperSymbol of S; :: thesis: ( Args o,A1 <> {} & Args o,A2 <> {} implies for i being Element of NAT st i in dom (the_arity_of o) holds
for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i) )
assume A1: ( Args o,A1 <> {} & Args o,A2 <> {} ) ; :: thesis: for i being Element of NAT st i in dom (the_arity_of o) holds
for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i)
let i be Element of NAT ; :: thesis: ( i in dom (the_arity_of o) implies for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i) )
assume i in dom (the_arity_of o) ; :: thesis: for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i)
then ( the Sorts of A1 . ((the_arity_of o) /. i) <> {} & the Sorts of A2 . ((the_arity_of o) /. i) <> {} ) by A1, Th3;
hence for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i) by FUNCT_2:7; :: thesis: verum