let i be Element of NAT ; :: thesis: for g, f being FinSequence of CQC-WFF st i in dom (Sgm (seq (len g),(len f))) holds
(Sgm (seq (len g),(len f))) . i = (len g) + i
let g, f be FinSequence of CQC-WFF ; :: thesis: ( i in dom (Sgm (seq (len g),(len f))) implies (Sgm (seq (len g),(len f))) . i = (len g) + i )
assume i in dom (Sgm (seq (len g),(len f))) ; :: thesis: (Sgm (seq (len g),(len f))) . i = (len g) + i
then i in dom f by Th11;
then A1: ( 1 <= i & i <= len f ) by FINSEQ_3:27;
defpred S₁[ Element of NAT ] means ( 1 <= $1 & $1 <= len f implies for i being Element of NAT st 1 <= i & i <= $1 holds
(Sgm (seq (len g),(len f))) . i = (len g) + i );
A2: S₁[ 0 ] ;
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
assume A5: ( 1 <= k + 1 & k + 1 <= len f ) ; :: thesis: for i being Element of NAT st 1 <= i & i <= k + 1 holds
(Sgm (seq (len g),(len f))) . i = (len g) + i
let n be Element of NAT ; :: thesis: ( 1 <= n & n <= k + 1 implies (Sgm (seq (len g),(len f))) . n = (len g) + n )
assume A6: ( 1 <= n & n <= k + 1 ) ; :: thesis: (Sgm (seq (len g),(len f))) . n = (len g) + n
A7: ( n <= k implies (Sgm (seq (len g),(len f))) . n = (len g) + n ) by A4, A5, A6, NAT_1:13, XXREAL_0:2;

now

assume A8: n = k + 1 ; :: thesis: (Sgm (seq (len g),(len f))) . n = (len g) + n
dom (Sgm (seq (len g),(len f))) = dom f by Th11;
then n in dom (Sgm (seq (len g),(len f))) by A5, A8, FINSEQ_3:27;
then (Sgm (seq (len g),(len f))) . n in rng (Sgm (seq (len g),(len f))) by FUNCT_1:12;
then reconsider i = (Sgm (seq (len g),(len f))) . n as Element of NAT ;

A9: now

assume A10: i < (len g) + (k + 1) ; :: thesis: contradiction

A11: now

assume A12: k = 0 ; :: thesis: contradiction
then not i in seq (len g),(len f) by A10, Th1;
then A13: not i in rng (Sgm (seq (len g),(len f))) by Th12;
1 <= len f by A5, XXREAL_0:2;
then 1 in dom f by FINSEQ_3:27;
then 1 in dom (Sgm (seq (len g),(len f))) by Th11;
hence contradiction by A8, A12, A13, FUNCT_1:12; :: thesis: verum

end;

now

assume A14: k <> 0 ; :: thesis: contradiction
A15: i < ((len g) + k) + 1 by A10;
0 < k by A14;
then A16: ( 0 + 1 <= k & k <= k + 1 ) by NAT_1:13;
then A17: (Sgm (seq (len g),(len f))) . k = (len g) + k by A4, A5, XXREAL_0:2;
then reconsider j = (Sgm (seq (len g),(len f))) . k as Element of NAT ;
A18: ( 1 <= k & k < k + 1 & k + 1 <= len (Sgm (seq (len g),(len f))) ) by A5, A16, Th10, NAT_1:13;
( i <= j & seq (len g),(len f) c= Seg ((len g) + (len f)) ) by A15, A17, Th7, NAT_1:13;
hence contradiction by A8, A18, FINSEQ_1:def 13; :: thesis: verum

end;

hence contradiction by A11; :: thesis: verum

end;

now

assume A19: i > (len g) + (k + 1) ; :: thesis: contradiction
A20: 1 + (len g) <= (1 + (len g)) + k by NAT_1:11;
(len g) + (k + 1) <= (len f) + (len g) by A5, XREAL_1:8;
then (len g) + (k + 1) in seq (len g),(len f) by A20;
then (len g) + (k + 1) in rng (Sgm (seq (len g),(len f))) by Th12;
then consider l being Nat such that
A21: ( l in dom (Sgm (seq (len g),(len f))) & (Sgm (seq (len g),(len f))) . l = (len g) + (k + 1) ) by FINSEQ_2:11;

A22: now

assume A23: l <= k + 1 ; :: thesis: contradiction

now

assume A24: l <= k ; :: thesis: contradiction

now

assume 1 <= l ; :: thesis: contradiction
then (len g) + (k + 1) = (len g) + l by A4, A5, A21, A24, NAT_1:13, XXREAL_0:2;
hence contradiction by A24, NAT_1:13; :: thesis: verum

end;

hence contradiction by A21, FINSEQ_3:27; :: thesis: verum

end;

hence contradiction by A8, A19, A21, A23, NAT_1:8; :: thesis: verum

end;

A25: ( 1 <= n & n < l & l <= len (Sgm (seq (len g),(len f))) ) by A8, A21, A22, FINSEQ_3:27, NAT_1:11;
seq (len g),(len f) c= Seg ((len g) + (len f)) by Th7;
hence contradiction by A19, A21, A25, FINSEQ_1:def 13; :: thesis: verum

end;

hence (Sgm (seq (len g),(len f))) . n = (len g) + n by A8, A9, XXREAL_0:1; :: thesis: verum

end;

hence (Sgm (seq (len g),(len f))) . n = (len g) + n by A6, A7, NAT_1:8; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
hence (Sgm (seq (len g),(len f))) . i = (len g) + i by A1; :: thesis: verum