let X be set ; :: thesis: for x being object holds (X --> 0.) . x = 0
let x be object ; :: thesis: (X --> 0.) . x = 0
set M = X --> 0.;

per cases ( x in dom (X --> 0.) or not x in dom (X --> 0.) ) ;

suppose x in dom (X --> 0.) ; :: thesis: (X --> 0.) . x = 0

then x in X ;
hence (X --> 0.) . x = 0 by FUNCOP_1:7; :: thesis: verum

end;

suppose not x in dom (X --> 0.) ; :: thesis: (X --> 0.) . x = 0

then (X --> 0.) . x = 0 by FUNCT_1:def 2;
hence (X --> 0.) . x = 0 ; :: thesis: verum

end;

end;