set H = F ^ G;
thus
F ^ G is LinearCombination of A \/ B
verumproof
let i be
set ;
IDEAL_1:def 8 ( 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)
;
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
not
i in dom F
;
ex u, v being Element of R ex a being Element of A \/ B st (F ^ G) /. i = (u * a) * vthen 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;
verum end; end;
end;