ex x being Element of C st (UMF C) . x = 1

proof

take x = the Element of C; :: thesis: (UMF C) . x = 1
thus (UMF C) . x = 1 by FUNCT_3:def 3; :: thesis: verum

end;

hence UMF C is normalized ; :: thesis: verum