let E be non empty set ; :: thesis: for F being Subset of (E ^omega )
for TS being non empty transition-system of F
for P being RedSequence of ==>.-relation TS st ex x being set ex u being Element of E ^omega st P . 1 = [x,u] holds
for k being Nat st k in dom P holds
dim2 (P . k),E = (P . k) `2
let F be Subset of (E ^omega ); :: thesis: for TS being non empty transition-system of F
for P being RedSequence of ==>.-relation TS st ex x being set ex u being Element of E ^omega st P . 1 = [x,u] holds
for k being Nat st k in dom P holds
dim2 (P . k),E = (P . k) `2
let TS be non empty transition-system of F; :: thesis: for P being RedSequence of ==>.-relation TS st ex x being set ex u being Element of E ^omega st P . 1 = [x,u] holds
for k being Nat st k in dom P holds
dim2 (P . k),E = (P . k) `2
let P be RedSequence of ==>.-relation TS; :: thesis: ( ex x being set ex u being Element of E ^omega st P . 1 = [x,u] implies for k being Nat st k in dom P holds
dim2 (P . k),E = (P . k) `2 )
given x being set , u being Element of E ^omega such that A:
P . 1 = [x,u]
; :: thesis: for k being Nat st k in dom P holds
dim2 (P . k),E = (P . k) `2
let k be Nat; :: thesis: ( k in dom P implies dim2 (P . k),E = (P . k) `2 )
assume B:
k in dom P
; :: thesis: dim2 (P . k),E = (P . k) `2
per cases
( k > 1 or k <= 1 )
;
suppose H:
k > 1
;
:: thesis: dim2 (P . k),E = (P . k) `2 then consider l being
Nat such that E:
k = l + 1
by NAT_1:6;
F:
l >= 1
by E, H, NAT_1:19;
G:
k <= len P
by B, FINSEQ_3:27;
l <= k
by E, NAT_1:11;
then
l <= len P
by G, XXREAL_0:2;
then
l in dom P
by F, FINSEQ_3:27;
then
[(P . l),(P . k)] in ==>.-relation TS
by B, E, REWRITE1:def 2;
then C:
P . k in rng (==>.-relation TS)
by RELAT_1:20;
rng (==>.-relation TS) c= [:the carrier of TS,(E ^omega ):]
by RELAT_1:def 19;
then consider x1,
y1 being
set such that D:
(
x1 in the
carrier of
TS &
y1 in E ^omega &
P . k = [x1,y1] )
by C, ZFMISC_1:def 2;
thus
dim2 (P . k),
E = (P . k) `2
by D, DefDim2;
:: thesis: verum end;