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 Instruction-Location of S by A1, Def4;
A5: the Object-Kind of S . l = ObjectKind 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;

dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;
then ( dom (f * s) c= dom s & dom s c= dom the Object-Kind of S ) by Th80, RELAT_1:44;
then dom (f * s) c= dom the Object-Kind of S by XBOOLE_1:1;
then reconsider fs = f * s as PartState of S by A2, CARD_3:def 9;
fs is NAT -defined ;
hence s * f is NAT -defined PartState of S ; :: thesis: verum