set F = Macro i;
let l be Nat; :: according to AMISTD_1:def 9 :: thesis: ( not l in K367(NAT,(Macro i)) or NIC (((Macro i) /. l),l) c= K367(NAT,(Macro i)) )
A1: dom (Macro i) = {0,1} by COMPOS_1:61;
assume A2: l in dom (Macro i) ; :: thesis: NIC (((Macro i) /. l),l) c= K367(NAT,(Macro i))
per cases then ( l = 0 or l = 1 ) by COMPOS_1:60;
suppose A3: l = 0 ; :: thesis: NIC (((Macro i) /. l),l) c= K367(NAT,(Macro i))
then (Macro i) /. l = (Macro i) . 0 by A2, PARTFUN1:def 6
.= i by COMPOS_1:58 ;
then NIC (((Macro i) /. l),l) = {(0 + 1)} by A3, AMISTD_1:12;
hence NIC (((Macro i) /. l),l) c= dom (Macro i) by A1, ZFMISC_1:7; :: thesis: verum
end;
suppose A4: l = 1 ; :: thesis: NIC (((Macro i) /. l),l) c= K367(NAT,(Macro i))
then (Macro i) /. l = (Macro i) . 1 by A2, PARTFUN1:def 6
.= halt SCM+FSA by COMPOS_1:59 ;
then NIC (((Macro i) /. l),l) = {1} by A4, AMISTD_1:2;
hence NIC (((Macro i) /. l),l) c= dom (Macro i) by A1, ZFMISC_1:7; :: thesis: verum
end;
end;