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 - ((len f) + 1) & k in dom g holds
$2 = g . k ) );
A1: for i being Nat st i in Seg ((len f) + (len g)) holds
ex y being object st S₁[i,y]

proof

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

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

suppose C1: i <= len f ; :: thesis: 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 < (len f) + 1 by C1, NAT_1:13;
then i - ((len f) + 1) < ((len f) + 1) - ((len f) + 1) by XREAL_1:9;
then for k being Nat st k = i - ((len f) + 1) & k in dom g holds
f . i = g . k by INT_1:3;
hence ex y being object st S₁[i,y] by C2; :: thesis: verum

end;

suppose C1: i > len f ; :: thesis: ex y being object st S₁[i,y]

then not i in Seg (len f) by FINSEQ_1:1;
then C3: for k being Nat st k = i & k in dom f holds
g . (i - ((len f) + 1)) = f . k by FINSEQ_1:def 3;
i >= (len f) + 1 by C1, NAT_1:13;
then i - ((len f) + 1) >= ((len f) + 1) - ((len f) + 1) by XREAL_1:9;
then reconsider j = i - ((len f) + 1) as Nat by INT_1:3;
for k being Nat st k = i - ((len f) + 1) & k in dom g holds
g . (i - ((len f) + 1)) = g . k ;
hence ex y being object st S₁[i,y] by C3; :: thesis: verum

end;

end;

end;

consider p being FinSequence such that
A2: ( dom p = Seg ((len f) + (len g)) & ( for k being Nat st k in Seg ((len f) + (len g)) holds
S₁[k,p . k] ) ) from FINSEQ_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
B2: (len f) + 0 <= (len f) + (len g) by XREAL_1:6;
( 1 <= k & k <= len f ) by B1, FINSEQ_3:25;
then ( 1 <= k & k <= (len f) + (len g) ) by B2, XXREAL_0:2;
then k in dom p by A2;
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
k in Segm (len g) by B1;
then k < len g by NAT_1:44;
then len g >= k + 1 by NAT_1:13;
then ( (len f) + (len g) >= (len f) + (k + 1) & ((len f) + k) + 1 >= 0 + 1 ) by XREAL_1:6;
then ((len f) + 1) + k in dom p by A2;
then p . (((len f) + 1) + k) = g . ((((len f) + 1) + k) - ((len f) + 1)) by A2, B1;
hence p . (((len f) + k) + 1) = g . k ; :: thesis: verum

end;

take p ; :: thesis: ( dom p = Seg ((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 = Seg ((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