let E be non empty set ; :: thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st ex x being object 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 over F
for P being RedSequence of ==>.-relation TS st ex x being object 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 over F; :: thesis: for P being RedSequence of ==>.-relation TS st ex x being object 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 object 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 object , u being Element of E ^omega such that A1: 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 A2: k in dom P ; :: thesis: dim2 ((P . k),E) = (P . k) `2

per cases ( k > 1 or k <= 1 ) ;

suppose A3: k > 1 ; :: thesis: dim2 ((P . k),E) = (P . k) `2

A4: k <= len P by A2, FINSEQ_3:25;
consider l being Nat such that
A5: k = l + 1 by A3, NAT_1:6;
l <= k by A5, NAT_1:11;
then A6: l <= len P by A4, XXREAL_0:2;
l >= 1 by A3, A5, NAT_1:19;
then l in dom P by A6, FINSEQ_3:25;
then [(P . l),(P . k)] in ==>.-relation TS by A2, A5, REWRITE1:def 2;
then A7: P . k in rng (==>.-relation TS) by XTUPLE_0:def 13;
rng (==>.-relation TS) c= [: the carrier of TS,(E ^omega):] by RELAT_1:def 19;
then ex x1, y1 being object st
( x1 in the carrier of TS & y1 in E ^omega & P . k = [x1,y1] ) by A7, ZFMISC_1:def 2;
hence dim2 ((P . k),E) = (P . k) `2 by Def5; :: thesis: verum

end;

suppose A8: k <= 1 ; :: thesis: dim2 ((P . k),E) = (P . k) `2

k >= 1 by A2, FINSEQ_3:25;
then k = 1 by A8, XXREAL_0:1;
hence dim2 ((P . k),E) = (P . k) `2 by A1, Def5; :: thesis: verum

end;

end;