let N be set ; :: thesis: for S being AMI-Struct of N
for p1, p2 being NAT -defined PartState of S holds p1 +* p2 is NAT -defined
let S be AMI-Struct of N; :: thesis: for p1, p2 being NAT -defined PartState of S holds p1 +* p2 is NAT -defined
let p1, p2 be NAT -defined PartState of S; :: thesis: p1 +* p2 is NAT -defined
A1: dom (p1 +* p2) = (dom p1) \/ (dom p2) by FUNCT_4:def 1;
( dom p1 c= NAT & dom p2 c= NAT ) by RELAT_1:def 18;
hence dom (p1 +* p2) c= NAT by A1, XBOOLE_1:8; :: according to RELAT_1:def 18 :: thesis: verum