hereby :: thesis: ( ( for o1, o2 being Object of C1 st <^o1,o2^> <> {} holds
<^(F . o1),(F . o2)^> <> {} ) implies F is feasible )

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

end;

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