let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S holds dom p c= {(IC )} \/ (dom (DataPart p))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; :: thesis: for p being PartState of S holds dom p c= {(IC )} \/ (dom (DataPart p))
let p be PartState of S; :: thesis: dom p c= {(IC )} \/ (dom (DataPart p))
set S0 = Start-At (0,S);
per cases ( IC in dom p or not IC in dom p ) ;
suppose IC in dom p ; :: thesis: dom p c= {(IC )} \/ (dom (DataPart p))
hence dom p c= {(IC )} \/ (dom (DataPart p)) by Th24; :: thesis: verum
end;
suppose A1: not IC in dom p ; :: thesis: dom p c= {(IC )} \/ (dom (DataPart p))
A3: dom (p +* (Start-At (0,S))) = {(IC )} \/ (dom (DataPart (p +* (Start-At (0,S))))) by Th24, Th27
.= {(IC )} \/ (dom ((DataPart p) +* (DataPart (Start-At (0,S))))) by FUNCT_4:71
.= {(IC )} \/ (dom ((DataPart p) +* {})) by Th20
.= {(IC )} \/ (dom (DataPart p)) ;
now :: thesis: not dom p meets dom (Start-At (0,S))
assume dom p meets dom (Start-At (0,S)) ; :: thesis: contradiction
then consider x being object such that
A4: x in dom p and
A5: x in dom (Start-At (0,S)) by XBOOLE_0:3;
thus contradiction by A4, A1, A5, TARSKI:def 1; :: thesis: verum
end;
then p c= p +* (Start-At (0,S)) by FUNCT_4:32;
hence dom p c= {(IC )} \/ (dom (DataPart p)) by A3, RELAT_1:11; :: thesis: verum
end;
end;