consider i being object such that
A: ( i in dom f & f . i <> 0. R ) by REALALG2:def 4;
B: (f ^ g) . i <> 0. R by A, FINSEQ_1:def 7;
dom f c= dom (f ^ g) by FINSEQ_1:26;
hence not f ^ g is trivial by A, B, REALALG2:def 4; :: thesis: verum