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 12 :: 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