let P be PartState of S; :: thesis: ( P = f +* p implies not P is program-free )
assume P = f +* p ; :: thesis: not P is program-free
then A: P | NAT = (f | NAT) +* (p | NAT) by FUNCT_4:75;
p | NAT <> {} by Def29;
hence P | NAT <> {} by A; :: according to COMPOS_1:def 29 :: thesis: verum