let Al be QC-alphabet ; 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 ; 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; ( 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))))
; (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;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
assume that A5:
1
<= k + 1
and A6:
k + 1
<= len f
;
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;
( 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
;
(Sgm (seq ((len g),(len f)))) . n = (len g) + n
A9:
now ( n = k + 1 implies (Sgm (seq ((len g),(len f)))) . n = (len g) + n )assume A10:
n = k + 1
;
(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 not i < (len g) + (k + 1)assume A12:
i < (len g) + (k + 1)
;
contradictionA13:
now not k <> 0 assume
k <> 0
;
contradictionthen 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 ;
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 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, A16, FINSEQ_1:def 13;
verum end; hence
contradiction
by A13;
verum end; now 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)
;
contradictionA26:
( 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 13;
verum end; hence
(Sgm (seq ((len g),(len f)))) . n = (len g) + n
by A10, A11, XXREAL_0:1;
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;
verum
end;
A27:
S1[ 0 ]
;
A28:
for n being Nat holds S1[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; verum