let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being AMI-Struct of IL,N
for s being State of S
for p being FinPartState of S holds s | (dom p) is FinPartState of S
let N be with_non-empty_elements set ; :: thesis: for S being AMI-Struct of IL,N
for s being State of S
for p being FinPartState of S holds s | (dom p) is FinPartState of S
let S be AMI-Struct of IL,N; :: thesis: for s being State of S
for p being FinPartState of S holds s | (dom p) is FinPartState of S
let s be State of S; :: thesis: for p being FinPartState of S holds s | (dom p) is FinPartState of S
let p be FinPartState of S; :: thesis: s | (dom p) is FinPartState of S
A1: ( product the Object-Kind of S c= sproduct the Object-Kind of S & s in product the Object-Kind of S ) by CARD_3:67;
dom (s | (dom p)) = (dom s) /\ (dom p) by RELAT_1:90;
hence s | (dom p) is FinPartState of S by A1, CARD_3:81, FINSET_1:29; :: thesis: verum