let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for l being Nat
for p being PartState of S holds
( p is l -started iff Start-At (l,S) c= p )
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; :: thesis: for l being Nat
for p being PartState of S holds
( p is l -started iff Start-At (l,S) c= p )
let l be Nat; :: thesis: for p being PartState of S holds
( p is l -started iff Start-At (l,S) c= p )
let p be PartState of S; :: thesis: ( p is l -started iff Start-At (l,S) c= p )
thus ( p is l -started implies Start-At (l,S) c= p ) :: thesis: ( Start-At (l,S) c= p implies p is l -started )
proof
assume A2: p is l -started ; :: thesis: Start-At (l,S) c= p
IC in dom p by A2;
then A3: dom (Start-At (l,S)) c= dom p by ZFMISC_1:31;
for x being object st x in dom (Start-At (l,S)) holds
(Start-At (l,S)) . x = p . x
proof
let x be object ; :: thesis: ( x in dom (Start-At (l,S)) implies (Start-At (l,S)) . x = p . x )
assume A4: x in dom (Start-At (l,S)) ; :: thesis: (Start-At (l,S)) . x = p . x
hence (Start-At (l,S)) . x = IC (Start-At (l,S)) by TARSKI:def 1
.= l by FUNCOP_1:72
.= IC p by A2
.= p . x by A4, TARSKI:def 1 ;
:: thesis: verum
end;
hence Start-At (l,S) c= p by A3, GRFUNC_1:2; :: thesis: verum
end;
assume A5: Start-At (l,S) c= p ; :: thesis: p is l -started
then A6: dom (Start-At (l,S)) c= dom p by RELAT_1:11;
A7: IC in dom (Start-At (l,S)) by TARSKI:def 1;
hence IC in dom p by A6; :: according to MEMSTR_0:def 11 :: thesis: IC p = l
thus IC p = IC (Start-At (l,S)) by A5, A7, GRFUNC_1:2
.= l by FUNCOP_1:72 ; :: thesis: verum