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

hence m = F + G by A1, A3, FUNCT_1:2; :: thesis: verum

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

dom m = the carrier of T
by FUNCT_2:def 1;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;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

hence m = F + G by A1, A3, FUNCT_1:2; :: thesis: verum