set F = stop (Directed I);
let l be Nat; :: according to AMISTD_1:def 9 :: thesis: ( not l in K339(NAT,(stop (Directed I))) or NIC (((stop (Directed I)) /. l),l) c= K339(NAT,(stop (Directed I))) )
assume A1: l in dom (stop (Directed I)) ; :: thesis: NIC (((stop (Directed I)) /. l),l) c= K339(NAT,(stop (Directed I)))
A2: card (Directed I) = card I by FUNCT_4:99;
then A3: dom (stop (Directed I)) = (dom I) \/ {(card I)} by AFINSQ_1:89;
A4: dom (Directed I) = dom I by FUNCT_4:99;
per cases ( l = card I or l <> card I ) ;
suppose l = card I ; :: thesis: NIC (((stop (Directed I)) /. l),l) c= K339(NAT,(stop (Directed I)))
then (stop (Directed I)) /. l = (stop (Directed I)) . (card (Directed I)) by A2, A1, PARTFUN1:def 6
.= halt SCM+FSA by COMPOS_1:64 ;
then NIC (((stop (Directed I)) /. l),l) = {l} by AMISTD_1:2;
hence NIC (((stop (Directed I)) /. l),l) c= dom (stop (Directed I)) by A1, ZFMISC_1:31; :: thesis: verum
end;
suppose l <> card I ; :: thesis: NIC (((stop (Directed I)) /. l),l) c= K339(NAT,(stop (Directed I)))
then not l in {(card I)} by TARSKI:def 1;
then A5: l in dom I by A3, A1, XBOOLE_0:def 3;
A6: (stop (Directed I)) /. l = (stop (Directed I)) . l by PARTFUN1:def 6, A1
.= (Directed I) . l by A4, A5, AFINSQ_1:def 3 ;
A7: dom I c= dom (stop (Directed I)) by A3, XBOOLE_1:7;
card I in {(card I)} by TARSKI:def 1;
then A8: card I in dom (stop (Directed I)) by A3, XBOOLE_0:def 3;
per cases ( I . l = halt SCM+FSA or I . l <> halt SCM+FSA ) ;
suppose I . l <> halt SCM+FSA ; :: thesis: NIC (((stop (Directed I)) /. l),l) c= K339(NAT,(stop (Directed I)))
then A9: (Directed I) . l = I . l by FUNCT_4:105
.= I /. l by A5, PARTFUN1:def 6 ;
NIC ((I /. l),l) c= dom I by A5, AMISTD_1:def 9;
then NIC ((I /. l),l) c= dom (stop (Directed I)) by A7, XBOOLE_1:1;
hence NIC (((stop (Directed I)) /. l),l) c= dom (stop (Directed I)) by A6, A9; :: thesis: verum
end;
end;
end;
end;