set IT = STC N;
set Ok = the Object-Kind of (STC N);
A1:
NAT in {NAT}
by TARSKI:def 1;
dom (NAT .--> NAT) = {NAT}
by FUNCOP_1:19;
then A2:
NAT in dom (NAT .--> NAT)
by TARSKI:def 1;
the Object-Kind of (STC N) . NAT =
((NAT --> {[1,0,0],[0,0,0]}) +* (NAT .--> NAT)) . NAT
by Def11
.=
(NAT .--> NAT) . NAT
by A2, FUNCT_4:14
.=
NAT
by A1, FUNCOP_1:13
;
then
ObjectKind (IC ) = NAT
by Def11;
hence
STC N is IC-Ins-separated
by COMPOS_1:def 6; ( STC N is definite & STC N is realistic )
A3:
the Instructions of (STC N) = {[1,0,0],[0,0,0]}
by Def11;
thus
STC N is definite
STC N is realistic proof
let l be
Element of
NAT ;
COMPOS_1:def 8 the Object-Kind of (STC N) . l = the Instructions of (STC N)
dom (NAT .--> NAT) = {NAT}
by FUNCOP_1:19;
then A4:
not
l in dom (NAT .--> NAT)
by TARSKI:def 1;
thus the
Object-Kind of
(STC N) . l =
((NAT --> {[1,0,0],[0,0,0]}) +* (NAT .--> NAT)) . l
by Def11
.=
(NAT --> {[1,0,0],[0,0,0]}) . l
by A4, FUNCT_4:12
.=
the
Instructions of
(STC N)
by A3, FUNCOP_1:13
;
verum
end;
thus
not the ZeroF of (STC N) in NAT
by Def11; COMPOS_1:def 12 verum