reconsider f = {} as Function ;

take f ; :: thesis: f is Univ_Alg-yielding

let x be object ; :: according to PRALG_1:def 10 :: thesis: ( x in dom f implies f . x is Universal_Algebra )

thus ( x in dom f implies f . x is Universal_Algebra ) ; :: thesis: verum

take f ; :: thesis: f is Univ_Alg-yielding

let x be object ; :: according to PRALG_1:def 10 :: thesis: ( x in dom f implies f . x is Universal_Algebra )

thus ( x in dom f implies f . x is Universal_Algebra ) ; :: thesis: verum