let S be non empty non void ManySortedSign ; :: thesis: for A1, A2 being MSAlgebra over 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 over 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 that
A1: Args (o,A1) <> {} and
A2: 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 A3: 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 A4: the Sorts of A2 . ((the_arity_of o) /. i) <> {} by A2, Th3;
the Sorts of A1 . ((the_arity_of o) /. i) <> {} by A1, A3, 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 A4, FUNCT_2:5; :: thesis: verum