let I be set ; :: thesis: for C being Category
for f being Morphism of C
for F being Function of I, the carrier' of C st doms F = I --> (cod f) holds
( doms (F * f) = I --> (dom f) & cods (F * f) = cods F )
let C be Category; :: thesis: for f being Morphism of C
for F being Function of I, the carrier' of C st doms F = I --> (cod f) holds
( doms (F * f) = I --> (dom f) & cods (F * f) = cods F )
let f be Morphism of C; :: thesis: for F being Function of I, the carrier' of C st doms F = I --> (cod f) holds
( doms (F * f) = I --> (dom f) & cods (F * f) = cods F )
let F be Function of I, the carrier' of C; :: thesis: ( doms F = I --> (cod f) implies ( doms (F * f) = I --> (dom f) & cods (F * f) = cods F ) )
assume A1: doms F = I --> (cod f) ; :: thesis: ( doms (F * f) = I --> (dom f) & cods (F * f) = cods F )
now :: thesis: for x being set st x in I holds
(doms (F * f)) /. x = (I --> (dom f)) /. x
let x be set ; :: thesis: ( x in I implies (doms (F * f)) /. x = (I --> (dom f)) /. x )
assume A2: x in I ; :: thesis: (doms (F * f)) /. x = (I --> (dom f)) /. x
then A3: dom (F /. x) = (I --> (cod f)) /. x by A1, Def1
.= cod f by A2, Th2 ;
thus (doms (F * f)) /. x = dom ((F * f) /. x) by A2, Def1
.= dom ((F /. x) (*) f) by A2, Def5
.= dom f by A3, CAT_1:17
.= (I --> (dom f)) /. x by A2, Th2 ; :: thesis: verum
end;
hence doms (F * f) = I --> (dom f) by Th1; :: thesis: cods (F * f) = cods F
now :: thesis: for x being set st x in I holds
(cods F) /. x = (cods (F * f)) /. x
let x be set ; :: thesis: ( x in I implies (cods F) /. x = (cods (F * f)) /. x )
assume A4: x in I ; :: thesis: (cods F) /. x = (cods (F * f)) /. x
then A5: dom (F /. x) = (I --> (cod f)) /. x by A1, Def1
.= cod f by A4, Th2 ;
thus (cods F) /. x = cod (F /. x) by A4, Def2
.= cod ((F /. x) (*) f) by A5, CAT_1:17
.= cod ((F * f) /. x) by A4, Def5
.= (cods (F * f)) /. x by A4, Def2 ; :: thesis: verum
end;
hence cods (F * f) = cods F by Th1; :: thesis: verum