let I be non empty set ; :: thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being set st x in rng (Frege (A ?. o)) holds
x is Function
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being set st x in rng (Frege (A ?. o)) holds
x is Function
let A be MSAlgebra-Family of I,S; :: thesis: for o being OperSymbol of S
for x being set st x in rng (Frege (A ?. o)) holds
x is Function
let o be OperSymbol of S; :: thesis: for x being set st x in rng (Frege (A ?. o)) holds
x is Function
let x be set ; :: thesis: ( x in rng (Frege (A ?. o)) implies x is Function )
assume x in rng (Frege (A ?. o)) ; :: thesis: x is Function
then ex y being object st
( y in dom (Frege (A ?. o)) & (Frege (A ?. o)) . y = x ) by FUNCT_1:def 3;
hence x is Function ; :: thesis: verum