let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of IL,N
for p being FinPartState of S
for s being State of S st IC S in dom p & p c= s holds
IC p = IC s
let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of IL,N
for p being FinPartState of S
for s being State of S st IC S in dom p & p c= s holds
IC p = IC s
let S be non empty IC-Ins-separated AMI-Struct of IL,N; :: thesis: for p being FinPartState of S
for s being State of S st IC S in dom p & p c= s holds
IC p = IC s
let p be FinPartState of S; :: thesis: for s being State of S st IC S in dom p & p c= s holds
IC p = IC s
let s be State of S; :: thesis: ( IC S in dom p & p c= s implies IC p = IC s )
assume that
A1: IC S in dom p and
A2: p c= s ; :: thesis: IC p = IC s
thus IC p = p . (IC S) by A1, Def43
.= IC s by A1, A2, GRFUNC_1:8 ; :: thesis: verum