let F be Function; :: thesis: ( F is NAT -defined & F is the Instructions of S -valued implies F is the Object-Kind of S -compatible )
assume A1: ( F is NAT -defined & F is the Instructions of S -valued ) ; :: thesis: F is the Object-Kind of S -compatible
let x be set ; :: according to FUNCT_1:def 20 :: thesis: ( not x in proj1 F or F . x in the Object-Kind of S . x )
assume A2: x in dom F ; :: thesis: F . x in the Object-Kind of S . x
A3: dom F c= NAT by A1, RELAT_1:def 18;
A4: rng F c= the Instructions of S by A1, RELAT_1:def 19;
F . x in rng F by A2, FUNCT_1:12;
then F . x in the Instructions of S by A4;
hence F . x in the Object-Kind of S . x by A3, A2, Def8; :: thesis: verum