let F be Function; :: thesis: ( F is TopStruct-yielding implies F is 1-sorted-yielding )
assume A1: F is TopStruct-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