A1: dom (f * s) c= dom s by RELAT_1:44;
dom s c= IL by RELAT_1:def 18;
then A2: dom (f * s) c= IL by A1, XBOOLE_1:1;
dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;
then dom s c= dom the Object-Kind of S by Th80;
then A3: dom (f * s) c= dom the Object-Kind of S by A1, XBOOLE_1:1;

now

let x be set ; :: thesis: ( x in dom (f * s) implies (f * s) . x in the Object-Kind of S . x )
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 A2, Def4;
A5: (f * s) . x in rng (f * s) by A4, FUNCT_1:def 5;
A6: rng f c= the Instructions of S by RELAT_1:def 19;
rng (f * s) c= rng f by RELAT_1:45;
then A7: rng (f * s) c= the Instructions of S by A6, XBOOLE_1:1;
the Object-Kind of S . l = ObjectKind l
.= the Instructions of S by Def14 ;
hence (f * s) . x in the Object-Kind of S . x by A5, A7; :: thesis: verum

end;

then reconsider fs = f * s as PartState of S by A3, CARD_3:def 9;
fs is IL -defined by A2, RELAT_1:def 18;
hence s * f is IL -defined PartState of S ; :: thesis: verum