set IT = STC N;

set Ok = the_Values_of (STC N);

A1: 0 in {0} by TARSKI:def 1;

A2: the_Values_of (STC N) = the ValuesF of (STC N) * the Object-Kind of (STC N)

.= the ValuesF of (STC N) * (0 .--> 0) by Def7

.= (N --> NAT) * (0 .--> 0) by Def7 ;

0 in N by MEASURE6:def 2;

then (the_Values_of (STC N)) . 0 = (0 .--> NAT) . 0 by A2, FUNCOP_1:89

.= NAT by A1, FUNCOP_1:7 ;

then Values (IC ) = NAT by Def7;

hence STC N is IC-Ins-separated ; :: thesis: verum

set Ok = the_Values_of (STC N);

A1: 0 in {0} by TARSKI:def 1;

A2: the_Values_of (STC N) = the ValuesF of (STC N) * the Object-Kind of (STC N)

.= the ValuesF of (STC N) * (0 .--> 0) by Def7

.= (N --> NAT) * (0 .--> 0) by Def7 ;

0 in N by MEASURE6:def 2;

then (the_Values_of (STC N)) . 0 = (0 .--> NAT) . 0 by A2, FUNCOP_1:89

.= NAT by A1, FUNCOP_1:7 ;

then Values (IC ) = NAT by Def7;

hence STC N is IC-Ins-separated ; :: thesis: verum