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

proof

let i be set ; :: according to IDEAL_1:def 8 :: thesis: ( i in dom (F ^ G) implies ex u, v being Element of R ex a being Element of A \/ B st (F ^ G) /. i = (u * a) * v )
assume A1: i in dom (F ^ G) ; :: thesis: ex u, v being Element of R ex a being Element of A \/ B st (F ^ G) /. i = (u * a) * v
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, v being Element of R ex a being Element of A \/ B st (F ^ G) /. i = (u * a) * v

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

end;

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

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, v being Element of R, b being Element of B such that
A8: G /. n = (u * b) * v by A5, Def8;
b in A \/ B by XBOOLE_0:def 3;
hence ex u, v being Element of R ex a being Element of A \/ B st (F ^ G) /. i = (u * a) * v by A1, A8, A7, PARTFUN1:def 6; :: thesis: verum

end;

end;

end;