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 S_{1}[ 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_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

A28: for n being Nat holds S_{1}[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

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 S

(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

S

proof

A27:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[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

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

end;assume A4: S

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 )

( n <= k implies (Sgm (seq ((len g),(len f)))) . n = (len g) + n )
by A4, A6, A7, NAT_1:13, XXREAL_0:2;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 ;

end;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

end;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 ;

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; :: thesis: verum

end;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 ;

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; :: thesis: verum

now :: thesis: not k = 0

hence
contradiction
by A13; :: thesis: verum
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;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

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

hence
(Sgm (seq ((len g),(len f)))) . n = (len g) + n
by A10, A11, XXREAL_0:1; :: thesis: verum
( 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

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; :: thesis: verum

end;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

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;A24: now :: thesis: not l <= k

assume
l <= k + 1
; :: thesis: contradictionassume A25:
l <= k
; :: thesis: contradiction

end;now :: thesis: not 1 <= l

hence
contradiction
by A20, FINSEQ_3:25; :: thesis: verumassume
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;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

hence contradiction by A10, A22, A21, A24, NAT_1:8; :: thesis: verum

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; :: thesis: verum

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

A28: for n being Nat holds S

1 <= i by A1, FINSEQ_3:25;

hence (Sgm (seq ((len g),(len f)))) . i = (len g) + i by A2, A28; :: thesis: verum