let o be Object of (STC N); :: according to AMISTD_4:def 2 :: thesis: not Values o is trivial
A1: the carrier of (STC N) = {0} by AMISTD_1:def 7;
A2: the Object-Kind of (STC N) = 0 .--> 0 by AMISTD_1:def 7;
per cases o in {0} by A1;
suppose A3: o in {0} ; :: thesis: not Values o is trivial
A4: the ValuesF of (STC N) = N --> NAT by AMISTD_1:def 7;
0 in N by MEASURE6:def 2;
then the_Values_of (STC N) = 0 .--> NAT by A2, A4, FUNCOP_1:89;
then Values o = (0 .--> NAT) . o
.= NAT by A3, FUNCOP_1:7 ;
hence not Values o is trivial ; :: thesis: verum
end;
end;