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 2
.=
the
Arrows of
C2 . (the ObjectMap of F . o1,o2)
by Th23
;
hence
<^(F . o1),(F . o2)^> <> {}
by A1, A2, Def12;
:: 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 12 :: 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 2
.=
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; :: thesis: verum