defpred S1[ object , object ] means for f, g being FinSequence st f = F . $1 & g = G . $1 holds
$2 = f ^ g;
A1: for i being object st i in (dom F) /\ (dom G) holds
ex u being object st S1[i,u]
proof
let i be object ; :: thesis: ( i in (dom F) /\ (dom G) implies ex u being object st S1[i,u] )
assume i in (dom F) /\ (dom G) ; :: thesis: ex u being object st S1[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: S1[i,f ^ g]
thus S1[i,f ^ g] ; :: thesis: verum
end;
consider H being Function such that
A2: ( dom H = (dom F) /\ (dom G) & ( for i being object st i in (dom F) /\ (dom G) holds
S1[i,H . i] ) ) from CLASSES1:sch 1(A1);
 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