defpred S₁[ set , set ] means for f, g being FinSequence st f = F . $1 & g = G . $1 holds
$2 = f ^ g;
A1: for i being set st i in (dom F) /\ (dom G) holds
ex u being set st S₁[i,u]

proof

let i be set ; :: thesis: ( i in (dom F) /\ (dom G) implies ex u being set st S₁[i,u] )
assume i in (dom F) /\ (dom G) ; :: thesis: ex u being set st S₁[i,u]
then ( i in dom F & i in dom G ) by XBOOLE_0:def 4;
then reconsider f = F . i, g = G . i as FinSequence by Def3;
take f ^ g ; :: thesis: S₁[i,f ^ g]
thus S₁[i,f ^ g] ; :: thesis: verum

end;

consider H being Function such that
A2: ( dom H = (dom F) /\ (dom G) & ( for i being set st i in (dom F) /\ (dom G) holds
S₁[i,H . i] ) ) from CLASSES1:sch 1(A1);
for x being set st x in dom H holds
H . x is FinSequence

proof

let x be set ; :: thesis: ( x in dom H implies H . x is FinSequence )
assume A3: x in dom H ; :: thesis: H . x is FinSequence
then x in dom F by A2, XBOOLE_0:def 4;
then reconsider f = F . x as FinSequence by Def3;
x in dom G by A2, A3, XBOOLE_0:def 4;
then reconsider g = G . x as FinSequence by Def3;
H . x = f ^ g by A2, A3;
hence H . x is FinSequence ; :: thesis: verum

end;

then reconsider H = H as FinSequence-yielding Function by Def3;
take H ; :: thesis: ( dom H = (dom F) /\ (dom G) & ( for i being set st i in dom H holds
for f, g being FinSequence st f = F . i & g = G . i holds
H . i = f ^ g ) )
thus ( dom H = (dom F) /\ (dom G) & ( for i being set st i in dom H holds
for f, g being FinSequence st f = F . i & g = G . i holds
H . i = f ^ g ) ) by A2; :: thesis: verum