let m be RealMap of T; :: thesis: ( m = F + G iff for t being Element of T holds m . t = (F . t) + (G . t) )
thus ( m = F + G implies for p being Element of T holds m . p = (F . p) + (G . p) ) by VALUED_1:1; :: thesis: ( ( for t being Element of T holds m . t = (F . t) + (G . t) ) implies m = F + G )
A1: dom (F + G) = (dom F) /\ (dom G) by VALUED_1:def 1
.= the carrier of T /\ (dom G) by FUNCT_2:def 1
.= the carrier of T /\ the carrier of T by FUNCT_2:def 1 ;
assume A2: for p being Element of T holds m . p = (F . p) + (G . p) ; :: thesis: m = F + G
A3: now :: thesis: for x being object st x in dom m holds
m . x = (F + G) . x
let x be object ; :: thesis: ( x in dom m implies m . x = (F + G) . x )
assume A4: x in dom m ; :: thesis: m . x = (F + G) . x
hence m . x = (F . x) + (G . x) by A2
.= (F + G) . x by A1, A4, VALUED_1:def 1 ;
:: thesis: verum
end;
dom m = the carrier of T by FUNCT_2:def 1;
hence m = F + G by A1, A3, FUNCT_1:2; :: thesis: verum