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 ]}) +* (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 o <> NAT ;
then not o in dom (NAT .--> NAT ) by A3, TARSKI:def 1;
then A5: ObjectKind o = (NAT --> {[1,0 ],[0 ,0 ]}) . o by A2, FUNCT_4:12
.= {[1,0 ],[0 ,0 ]} by A4, FUNCOP_1:13 ;
A6: [1,0 ] <> [0 ,0 ] by ZFMISC_1:33;
( [1,0 ] in {[1,0 ],[0 ,0 ]} & [0 ,0 ] in {[1,0 ],[0 ,0 ]} ) by 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;