A1: dom (f * s) c= NAT by RELAT_1:def 18;

A2: now

let x be set ; :: thesis: ( x in dom (f * s) implies (f * s) . x in the Object-Kind of S . x )
A3: rng (f * s) c= the Instructions of S by RELAT_1:def 19;
assume A4: x in dom (f * s) ; :: thesis: (f * s) . x in the Object-Kind of S . x
then reconsider l = x as Element of NAT by A1;
A5: the Object-Kind of S . l = the Instructions of S by Def14;
(f * s) . x in rng (f * s) by A4, FUNCT_1:def 5;
hence (f * s) . x in the Object-Kind of S . x by A3, A5; :: thesis: verum

end;

reconsider fs = f * s as PartState of S by A2, FUNCT_1:def 20;
fs is NAT -defined ;
hence s * f is NAT -defined PartState of ; :: thesis: verum