let f be Function; :: thesis: ( f is TolStr-yielding implies f is 1-sorted-yielding )
assume A1: f is TolStr-yielding ; :: thesis: f is 1-sorted-yielding
let x be object ; :: according to PRALG_1:def 12 :: thesis: ( not x in proj1 f or f . x is 1-sorted )
thus ( not x in proj1 f or f . x is 1-sorted ) by A1; :: thesis: verum