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

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

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

end;

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

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

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

end;

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