let IL be non empty set ; :: thesis: for N being set
for S being AMI-Struct of IL,N
for p1, p2 being programmed PartState of S holds p1 +* p2 is programmed
let N be set ; :: thesis: for S being AMI-Struct of IL,N
for p1, p2 being programmed PartState of S holds p1 +* p2 is programmed
let S be AMI-Struct of IL,N; :: thesis: for p1, p2 being programmed PartState of S holds p1 +* p2 is programmed
let p1, p2 be programmed PartState of S; :: thesis: p1 +* p2 is programmed
A1: ( dom p1 c= IL & dom p2 c= IL ) by Def40;
dom (p1 +* p2) = (dom p1) \/ (dom p2) by FUNCT_4:def 1;
hence dom (p1 +* p2) c= IL by A1, XBOOLE_1:8; :: according to AMI_1:def 40 :: thesis: verum