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