now :: thesis: for i being object st i in dom (f ^ g) holds
(f ^ g) . i = 0. R

let i be object ; :: thesis: ( i in dom (f ^ g) implies (f ^ g) . b₁ = 0. R )
assume i in dom (f ^ g) ; :: thesis: (f ^ g) . b₁ = 0. R

per cases then ( i in dom f or ex n being Nat st
( n in dom g & i = (len f) + n ) ) by FINSEQ_1:25;

suppose A: i in dom f ; :: thesis: (f ^ g) . b₁ = 0. R

then (f ^ g) . i = f . i by FINSEQ_1:def 7;
hence (f ^ g) . i = 0. R by A, REALALG2:def 4; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom g & i = (len f) + n ) ; :: thesis: (f ^ g) . b₁ = 0. R

then consider n being Nat such that
A: ( n in dom g & i = (len f) + n ) ;
(f ^ g) . i = g . n by A, FINSEQ_1:def 7;
hence (f ^ g) . i = 0. R by A, REALALG2:def 4; :: thesis: verum

end;

end;

end;

hence f ^ g is trivial by REALALG2:def 4; :: thesis: verum