let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al
for i being Nat st i in dom (Sgm (seq ((len g),(len f)))) holds
(Sgm (seq ((len g),(len f)))) . i = (len g) + i
let f, g be FinSequence of CQC-WFF Al; :: thesis: for i being Nat st i in dom (Sgm (seq ((len g),(len f)))) holds
(Sgm (seq ((len g),(len f)))) . i = (len g) + i
let i be Nat; :: thesis: ( i in dom (Sgm (seq ((len g),(len f)))) implies (Sgm (seq ((len g),(len f)))) . i = (len g) + i )
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len f implies for i being Nat st 1 <= i & i <= $1 holds
(Sgm (seq ((len g),(len f)))) . i = (len g) + i );
assume A1: 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 A2: i <= len f by FINSEQ_3:25;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
assume that
A5: 1 <= k + 1 and
A6: k + 1 <= len f ; :: thesis: for i being Nat st 1 <= i & i <= k + 1 holds
(Sgm (seq ((len g),(len f)))) . i = (len g) + i
let n be Nat; :: thesis: ( 1 <= n & n <= k + 1 implies (Sgm (seq ((len g),(len f)))) . n = (len g) + n )
assume that
A7: 1 <= n and
A8: n <= k + 1 ; :: thesis: (Sgm (seq ((len g),(len f)))) . n = (len g) + n

A9: now :: thesis: ( n = k + 1 implies (Sgm (seq ((len g),(len f)))) . n = (len g) + n )

assume A10: 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, A6, A10, FINSEQ_3:25;
then (Sgm (seq ((len g),(len f)))) . n in rng (Sgm (seq ((len g),(len f)))) by FUNCT_1:3;
then reconsider i = (Sgm (seq ((len g),(len f)))) . n as Element of NAT ;

A11: now :: thesis: not i < (len g) + (k + 1)

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

A13: now :: thesis: not k <> 0

assume k <> 0 ; :: thesis: contradiction
then A14: 0 + 1 <= k by NAT_1:13;
then A15: (Sgm (seq ((len g),(len f)))) . k = (len g) + k by A4, A6, NAT_1:13;
then reconsider j = (Sgm (seq ((len g),(len f)))) . k as Nat ;
A17: ( k < k + 1 & k + 1 <= len (Sgm (seq ((len g),(len f)))) ) by A6, Th10, NAT_1:13;
i < ((len g) + k) + 1 by A12;
then i <= j by A15, NAT_1:13;
hence contradiction by A10, A14, A17, FINSEQ_1:def 14; :: thesis: verum

end;

now :: thesis: not k = 0

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

end;

hence contradiction by A13; :: thesis: verum

end;

now :: thesis: not i > (len g) + (k + 1)

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

A23: now :: thesis: not l <= k + 1

A24: now :: thesis: not l <= k

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

now :: thesis: not 1 <= l

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

end;

hence contradiction by A20, FINSEQ_3:25; :: thesis: verum

end;

assume l <= k + 1 ; :: thesis: contradiction
hence contradiction by A10, A22, A21, A24, NAT_1:8; :: thesis: verum

end;

A26: ( 1 <= n & seq ((len g),(len f)) c= Seg ((len g) + (len f)) ) by A10, Th7, NAT_1:11;
l <= len (Sgm (seq ((len g),(len f)))) by A20, FINSEQ_3:25;
hence contradiction by A10, A22, A21, A23, A26, FINSEQ_1:def 14; :: thesis: verum

end;

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

end;

( n <= k implies (Sgm (seq ((len g),(len f)))) . n = (len g) + n ) by A4, A6, A7, NAT_1:13, XXREAL_0:2;
hence (Sgm (seq ((len g),(len f)))) . n = (len g) + n by A8, A9, NAT_1:8; :: thesis: verum

end;

A27: S₁[ 0 ] ;
A28: for n being Nat holds S₁[n] from NAT_1:sch 2(A27, A3);
1 <= i by A1, FINSEQ_3:25;
hence (Sgm (seq ((len g),(len f)))) . i = (len g) + i by A2, A28; :: thesis: verum