let o be Object of (STC N); :: according to AMI_7:def 2 :: thesis: not ObjectKind o is trivial
A1: the carrier of (STC N) = NAT \/ {NAT} by AMISTD_1:def 11;
A2: the Object-Kind of (STC N) = (NAT --> {[1,0,0],[0,0,0]}) +* (NAT .--> NAT) by AMISTD_1:def 11;
A3: dom (NAT .--> NAT) = {NAT} by FUNCOP_1:19;

per cases ( o in NAT or o in {NAT} ) by A1, XBOOLE_0:def 3;

suppose A4: o in NAT ; :: thesis: not ObjectKind o is trivial

then not o in dom (NAT .--> NAT) by A3, TARSKI:def 1;
then A5: ObjectKind o = (NAT --> {[1,0,0],[0,0,0]}) . o by A2, FUNCT_4:12
.= {[1,0,0],[0,0,0]} by A4, FUNCOP_1:13 ;
A6: [0,0,0] in {[1,0,0],[0,0,0]} by TARSKI:def 2;
( [1,0,0] <> [0,0,0] & [1,0,0] in {[1,0,0],[0,0,0]} ) by MCART_1:28, TARSKI:def 2;
hence not ObjectKind o is trivial by A5, A6, YELLOW_8:def 1; :: thesis: verum

end;

suppose A7: o in {NAT} ; :: thesis: not ObjectKind o is trivial

then ObjectKind o = (NAT .--> NAT) . o by A2, A3, FUNCT_4:14
.= NAT by A7, FUNCOP_1:13 ;
hence not ObjectKind o is trivial ; :: thesis: verum

end;

end;