hereby ( ( for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds
<^(F . o2),(F . o1)^> <> {} ) implies F is feasible )
assume A1:
F is
feasible
;
for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds
<^(F . o2),(F . o1)^> <> {} let o1,
o2 be
Object of
C1;
( <^o1,o2^> <> {} implies <^(F . o2),(F . o1)^> <> {} )assume A2:
<^o1,o2^> <> {}
;
<^(F . o2),(F . o1)^> <> {} <^(F . o2),(F . o1)^> =
the
Arrows of
C2 . (
(F . o2),
(F . o1))
by ALTCAT_1:def 1
.=
the
Arrows of
C2 . ( the ObjectMap of F . (o1,o2))
by Th23
;
hence
<^(F . o2),(F . o1)^> <> {}
by A1, A2;
verum
end;
assume A3:
for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds
<^(F . o2),(F . o1)^> <> {}
; F is feasible
let o1, o2 be Object of C1; FUNCTOR0:def 11 ( <^o1,o2^> <> {} implies the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {} )
assume A4:
<^o1,o2^> <> {}
; the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {}
<^(F . o2),(F . o1)^> =
the Arrows of C2 . ((F . o2),(F . o1))
by ALTCAT_1:def 1
.=
the Arrows of C2 . ( the ObjectMap of F . (o1,o2))
by Th23
;
hence
the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) <> {}
by A3, A4; verum