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