set H = F ^ G;
thus F ^ G is RightLinearCombination of A \/ B :: thesis: verum

proof

let i be set ; :: according to IDEAL_1:def 10 :: thesis: ( i in dom (F ^ G) implies ex u being Element of R ex a being Element of A \/ B st (F ^ G) /. i = a * u )
assume A1: i in dom (F ^ G) ; :: thesis: ex u being Element of R ex a being Element of A \/ B st (F ^ G) /. i = a * u
then reconsider i = i as Element of NAT ;

per cases ( i in dom F or not i in dom F ) ;

suppose A2: i in dom F ; :: thesis: ex u being Element of R ex a being Element of A \/ B st (F ^ G) /. i = a * u

then A3: ( F /. i = F . i & F . i = (F ^ G) . i ) by FINSEQ_1:def 7, PARTFUN1:def 6;
consider u being Element of R, a being Element of A such that
A4: F /. i = a * u by A2, Def10;
a in A \/ B by XBOOLE_0:def 3;
hence ex u being Element of R ex a being Element of A \/ B st (F ^ G) /. i = a * u by A1, A4, A3, PARTFUN1:def 6; :: thesis: verum

end;

suppose not i in dom F ; :: thesis: ex u being Element of R ex a being Element of A \/ B st (F ^ G) /. i = a * u

then consider n being Nat such that
A5: n in dom G and
A6: i = (len F) + n by A1, FINSEQ_1:25;
A7: ( G /. n = G . n & G . n = (F ^ G) . i ) by A5, A6, FINSEQ_1:def 7, PARTFUN1:def 6;
consider u being Element of R, b being Element of B such that
A8: G /. n = b * u by A5, Def10;
b in A \/ B by XBOOLE_0:def 3;
hence ex u being Element of R ex a being Element of A \/ B st (F ^ G) /. i = a * u by A1, A8, A7, PARTFUN1:def 6; :: thesis: verum

end;

end;

end;