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 Z0: ( 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 Z: x in dom F ; :: thesis: F . x in the Object-Kind of S . x
dom F c= NAT by RELAT_1:def 18, Z0;
then A: x in NAT by Z;
C: rng F c= the Instructions of S by RELAT_1:def 19, Z0;
F . x in rng F by Z, FUNCT_1:12;
then B: F . x in the Instructions of S by C;
the Object-Kind of S . x = the Instructions of S by A, Def14;
hence F . x in the Object-Kind of S . x by B; :: thesis: verum