let x be object ; :: according to PRE_POLY:def 3 :: thesis: ( x in dom (F ^^ G) implies (F ^^ G) . x is FinSequence )
assume A1: x in dom (F ^^ G) ; :: thesis: (F ^^ G) . x is FinSequence
then A2: x in (dom F) /\ (dom G) by Def4;
then x in dom F by XBOOLE_0:def 4;
then reconsider f = F . x as FinSequence by Def3;
x in dom G by A2, XBOOLE_0:def 4;
then reconsider g = G . x as FinSequence by Def3;
(F ^^ G) . x = f ^ g by A1, Def4;
hence (F ^^ G) . x is FinSequence ; :: thesis: verum