let a be Real; :: thesis: for X being non empty set holds
( (X --> 0) + (X --> 0) = X --> 0 & a (#) (X --> 0) = X --> 0 )
let X be non empty set ; :: thesis: ( (X --> 0) + (X --> 0) = X --> 0 & a (#) (X --> 0) = X --> 0 )
set g1 = X --> 0;
set g2 = X --> 0;

A1: now :: thesis: for x being Element of X st x in dom (a (#) (X --> 0)) holds
(a (#) (X --> 0)) . x = (X --> 0) . x

let x be Element of X; :: thesis: ( x in dom (a (#) (X --> 0)) implies (a (#) (X --> 0)) . x = (X --> 0) . x )
assume x in dom (a (#) (X --> 0)) ; :: thesis: (a (#) (X --> 0)) . x = (X --> 0) . x
then (a (#) (X --> 0)) . x = a * ((X --> 0) . x) by VALUED_1:def 5;
then (a (#) (X --> 0)) . x = a * 0 by FUNCOP_1:7;
hence (a (#) (X --> 0)) . x = (X --> 0) . x by FUNCOP_1:7; :: thesis: verum

end;

A2: dom ((X --> 0) + (X --> 0)) = (dom (X --> 0)) /\ (dom (X --> 0)) by VALUED_1:def 1;

now :: thesis: for x being Element of X st x in dom (X --> 0) holds
((X --> 0) + (X --> 0)) . x = (X --> 0) . x

let x be Element of X; :: thesis: ( x in dom (X --> 0) implies ((X --> 0) + (X --> 0)) . x = (X --> 0) . x )
assume x in dom (X --> 0) ; :: thesis: ((X --> 0) + (X --> 0)) . x = (X --> 0) . x
then ((X --> 0) + (X --> 0)) . x = ((X --> 0) . x) + ((X --> 0) . x) by A2, VALUED_1:def 1;
then ((X --> 0) + (X --> 0)) . x = 0 + ((X --> 0) . x) by FUNCOP_1:7;
hence ((X --> 0) + (X --> 0)) . x = (X --> 0) . x ; :: thesis: verum

end;

hence (X --> 0) + (X --> 0) = X --> 0 by A2, PARTFUN1:5; :: thesis: a (#) (X --> 0) = X --> 0
dom (a (#) (X --> 0)) = dom (X --> 0) by VALUED_1:def 5;
hence a (#) (X --> 0) = X --> 0 by A1, PARTFUN1:5; :: thesis: verum