defpred S₁[ Nat, object ] means ( ( for k being Nat st k = $1 & k in dom f holds
$2 = f . k ) & ( for k being Nat st k = ($1 + 1) - (len f) & k in dom g holds
$2 = g . k ) );
A1: for i being Nat st i in (len f) + (len g) holds
ex y being object st S₁[i,y]

proof

let i be Nat; :: thesis: ( i in (len f) + (len g) implies ex y being object st S₁[i,y] )

per cases ( i < len f or i >= len f ) ;

suppose C1: i < len f ; :: thesis: ( i in (len f) + (len g) implies ex y being object st S₁[i,y] )

C2: for k being Nat st k = i & k in dom f holds
f . i = f . k ;
i + (1 - (len f)) < (len f) + (1 - (len f)) by C1, XREAL_1:6;
then not (i + 1) - (len f) in Seg (len g) by FINSEQ_1:1;
then for k being Nat st k = (i - (len f)) + 1 & k in dom g holds
f . i = g . k by FINSEQ_1:def 3;
hence ( i in (len f) + (len g) implies ex y being object st S₁[i,y] ) by C2; :: thesis: verum

end;

suppose C1: i >= len f ; :: thesis: ( i in (len f) + (len g) implies ex y being object st S₁[i,y] )

then not i in Segm (len f) by NAT_1:44;
then C3: for k being Nat st k = i & k in dom f holds
g . ((i + 1) - (len f)) = f . k ;
i + (1 - (len f)) >= (len f) + (1 - (len f)) by C1, XREAL_1:6;
then reconsider j = (i + 1) - (len f) as non zero Nat ;
for k being Nat st k = (i + 1) - (len f) & k in dom g holds
g . ((i + 1) - (len f)) = g . k ;
hence ( i in (len f) + (len g) implies ex y being object st S₁[i,y] ) by C3; :: thesis: verum

end;

end;

end;

consider p being XFinSequence such that
A2: ( dom p = (len f) + (len g) & ( for k being Nat st k in (len f) + (len g) holds
S₁[k,p . k] ) ) from AFINSQ_1:sch 1(A1);
A3: for k being Nat st k in dom f holds
p . k = f . k

proof

let k be Nat; :: thesis: ( k in dom f implies p . k = f . k )
assume B1: k in dom f ; :: thesis: p . k = f . k
then k in Segm (len f) ;
then ( k < len f & (len f) + 0 <= (len f) + (len g) ) by NAT_1:44, XREAL_1:6;
then k < (len f) + (len g) by XXREAL_0:2;
then k in Segm ((len f) + (len g)) by NAT_1:44;
hence p . k = f . k by A2, B1; :: thesis: verum

end;

A4: for k being Nat st k in dom g holds
p . (((len f) + k) - 1) = g . k

proof

let k be Nat; :: thesis: ( k in dom g implies p . (((len f) + k) - 1) = g . k )
assume B1: k in dom g ; :: thesis: p . (((len f) + k) - 1) = g . k
then B2: ( 1 <= k & k <= len g ) by FINSEQ_3:25;
then reconsider j = k - 1 as Nat ;
( ((len g) - 1) + 1 > ((len g) - 1) + 0 & (len g) - 1 >= j ) by B2, XREAL_1:6, XREAL_1:9;
then len g > j by XXREAL_0:2;
then (len f) + j in Segm ((len f) + (len g)) by NAT_1:44, XREAL_1:6;
then p . (((len f) + k) - 1) = g . (((((len f) + k) - 1) + 1) - (len f)) by A2, B1;
hence p . (((len f) + k) - 1) = g . k ; :: thesis: verum

end;

take p ; :: thesis: ( dom p = (len f) + (len g) & ( for k being Nat st k in dom f holds
p . k = f . k ) & ( for k being Nat st k in dom g holds
p . (((len f) + k) - 1) = g . k ) )
thus ( dom p = (len f) + (len g) & ( for k being Nat st k in dom f holds
p . k = f . k ) & ( for k being Nat st k in dom g holds
p . (((len f) + k) - 1) = g . k ) ) by A2, A3, A4; :: thesis: verum