consider l1, l2 being Element of NAT such that
A1: l1 <> l2 by YELLOW_8:def 1;
reconsider l1 = l1, l2 = l2 as Element of NAT ;
consider I being Instruction of S;
take f = (l1,l2) --> (I,I); :: thesis: ( not f is trivial & f is NAT -defined )
thus not f is trivial :: thesis: f is NAT -defined

proof

f = {[l1,I],[l2,I]} by A1, FUNCT_4:71;
then reconsider x = [l1,I], y = [l2,I] as Element of f by TARSKI:def 2;
take x ; :: according to YELLOW_8:def 1 :: thesis: not for b₁ being Element of f holds x = b₁
take y ; :: thesis: not x = y
thus not x = y by A1, ZFMISC_1:33; :: thesis: verum

end;

let a be set ; :: according to RELAT_1:def 18,TARSKI:def 3 :: thesis: ( not a in proj1 f or a in NAT )
assume a in dom f ; :: thesis: a in NAT
then a in {l1,l2} by FUNCT_4:65;
then ( a = l1 or a = l2 ) by TARSKI:def 2;
hence a in NAT ; :: thesis: verum