let f be Function; :: thesis: ( f is multMagma-yielding implies f is 1-sorted-yielding )

assume A1: f is multMagma-yielding ; :: thesis: f is 1-sorted-yielding

let x be object ; :: according to PRALG_1:def 11 :: thesis: ( not x in dom f or f . x is 1-sorted )

assume x in dom f ; :: thesis: f . x is 1-sorted

then f . x in rng f by FUNCT_1:def 3;

hence f . x is 1-sorted by A1; :: thesis: verum

assume A1: f is multMagma-yielding ; :: thesis: f is 1-sorted-yielding

let x be object ; :: according to PRALG_1:def 11 :: thesis: ( not x in dom f or f . x is 1-sorted )

assume x in dom f ; :: thesis: f . x is 1-sorted

then f . x in rng f by FUNCT_1:def 3;

hence f . x is 1-sorted by A1; :: thesis: verum