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 ;
B1: dom ((X --> 0 ) + (X --> 0 )) = (dom (X --> 0 )) /\ (dom (X --> 0 )) by VALUED_1:def 1;

now

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 B1, VALUED_1:def 1;
then ((X --> 0 ) + (X --> 0 )) . x = 0 + ((X --> 0 ) . x) by FUNCOP_1:13;
hence ((X --> 0 ) + (X --> 0 )) . x = (X --> 0 ) . x ; :: thesis: verum

end;

hence (X --> 0 ) + (X --> 0 ) = X --> 0 by B1, PARTFUN1:34; :: thesis: a (#) (X --> 0 ) = X --> 0
B2: dom (a (#) (X --> 0 )) = dom (X --> 0 ) by VALUED_1:def 5;

now

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:13;
hence (a (#) (X --> 0 )) . x = (X --> 0 ) . x by FUNCOP_1:13; :: thesis: verum

end;

hence a (#) (X --> 0 ) = X --> 0 by B2, PARTFUN1:34; :: thesis: verum