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