let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty ManySortedSet of the carrier of S
for f being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S
for o being OperSymbol of S
for d being Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) holds f +* (o,d) is ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S
let A be non-empty ManySortedSet of the carrier of S; :: thesis: for f being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S
for o being OperSymbol of S
for d being Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) holds f +* (o,d) is ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S
let f be ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S; :: thesis: for o being OperSymbol of S
for d being Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) holds f +* (o,d) is ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S
let o be OperSymbol of S; :: thesis: for d being Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) holds f +* (o,d) is ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S
let d be Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o); :: thesis: f +* (o,d) is ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S
let x be object ; :: according to PBOOLE:def 15 :: thesis: ( not x in the carrier' of S or (f +* (o,d)) . x is Element of bool [:(((A #) * the Arity of S) . x),((A * the ResultSort of S) . x):] )
assume x in the carrier' of S ; :: thesis: (f +* (o,d)) . x is Element of bool [:(((A #) * the Arity of S) . x),((A * the ResultSort of S) . x):]
then reconsider x = x as OperSymbol of S ;
dom f = the carrier' of S by PARTFUN1:def 2;
then ( ( x = o implies (f +* (o,d)) . x = d ) & ( x <> o implies (f +* (o,d)) . x = f . x ) ) by FUNCT_7:31, FUNCT_7:32;
hence (f +* (o,d)) . x is Element of bool [:(((A #) * the Arity of S) . x),((A * the ResultSort of S) . x):] ; :: thesis: verum