let Al be QC-alphabet ; :: thesis: for i being Element of NAT
for f, g being FinSequence of CQC-WFF Al st i in dom (Sgm (seq ((len g),(len f)))) holds
(Sgm (seq ((len g),(len f)))) . i = (len g) + i

let i be Element of NAT ; :: thesis: for f, g being FinSequence of CQC-WFF Al 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: ( i in dom (Sgm (seq ((len g),(len f)))) implies (Sgm (seq ((len g),(len f)))) . i = (len g) + i )
defpred S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[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 ;
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 ;
then reconsider j = (Sgm (seq ((len g),(len f)))) . k as Nat ;
A16: seq ((len g),(len f)) c= Seg ((len g) + (len f)) by Th7;
A17: ( k < k + 1 & k + 1 <= len (Sgm (seq ((len g),(len f)))) ) by ;
i < ((len g) + k) + 1 by A12;
then i <= j by ;
hence contradiction by A10, A14, A17, A16, FINSEQ_1:def 13; :: thesis: verum
end;
now :: thesis: not k = 0
1 <= len f by ;
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 ;
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 ;
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 ;
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 ;
l <= len (Sgm (seq ((len g),(len f)))) by ;
hence contradiction by A10, A22, A21, A23, A26, FINSEQ_1:def 13; :: thesis: verum
end;
hence (Sgm (seq ((len g),(len f)))) . n = (len g) + n by ; :: thesis: verum
end;
( n <= k implies (Sgm (seq ((len g),(len f)))) . n = (len g) + n ) by ;
hence (Sgm (seq ((len g),(len f)))) . n = (len g) + n by ; :: thesis: verum
end;
A27: S1[ 0 ] ;
A28: for n being Nat holds S1[n] from NAT_1:sch 2(A27, A3);
1 <= i by ;
hence (Sgm (seq ((len g),(len f)))) . i = (len g) + i by ; :: thesis: verum