set S = the 1-sorted ;
take f = {{}} --> the 1-sorted ; :: thesis: ( not f is empty & f is constant & f is 1-sorted-yielding )
thus not f is empty ; :: thesis: ( f is constant & f is 1-sorted-yielding )
thus f is constant ; :: 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 )
assume x in dom f ; :: thesis: f . x is 1-sorted
hence f . x is 1-sorted by FUNCOP_1:7; :: thesis: verum