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 cods F = I --> (dom f) holds

( doms (f * F) = doms F & cods (f * F) = I --> (cod f) )

let C be Category; :: thesis: for f being Morphism of C

for F being Function of I, the carrier' of C st cods F = I --> (dom f) holds

( doms (f * F) = doms F & cods (f * F) = I --> (cod f) )

let f be Morphism of C; :: thesis: for F being Function of I, the carrier' of C st cods F = I --> (dom f) holds

( doms (f * F) = doms F & cods (f * F) = I --> (cod f) )

let F be Function of I, the carrier' of C; :: thesis: ( cods F = I --> (dom f) implies ( doms (f * F) = doms F & cods (f * F) = I --> (cod f) ) )

assume A1: cods F = I --> (dom f) ; :: thesis: ( doms (f * F) = doms F & cods (f * F) = I --> (cod f) )

for f being Morphism of C

for F being Function of I, the carrier' of C st cods F = I --> (dom f) holds

( doms (f * F) = doms F & cods (f * F) = I --> (cod f) )

let C be Category; :: thesis: for f being Morphism of C

for F being Function of I, the carrier' of C st cods F = I --> (dom f) holds

( doms (f * F) = doms F & cods (f * F) = I --> (cod f) )

let f be Morphism of C; :: thesis: for F being Function of I, the carrier' of C st cods F = I --> (dom f) holds

( doms (f * F) = doms F & cods (f * F) = I --> (cod f) )

let F be Function of I, the carrier' of C; :: thesis: ( cods F = I --> (dom f) implies ( doms (f * F) = doms F & cods (f * F) = I --> (cod f) ) )

assume A1: cods F = I --> (dom f) ; :: thesis: ( doms (f * F) = doms F & cods (f * F) = I --> (cod f) )

now :: thesis: for x being set st x in I holds

(doms F) /. x = (doms (f * F)) /. x

hence
doms (f * F) = doms F
by Th1; :: thesis: cods (f * F) = I --> (cod f)(doms F) /. x = (doms (f * F)) /. x

let x be set ; :: thesis: ( x in I implies (doms F) /. x = (doms (f * F)) /. x )

assume A2: x in I ; :: thesis: (doms F) /. x = (doms (f * F)) /. x

then A3: cod (F /. x) = (I --> (dom f)) /. x by A1, Def2

.= dom f by A2, Th2 ;

thus (doms F) /. x = dom (F /. x) by A2, Def1

.= dom (f (*) (F /. x)) by A3, CAT_1:17

.= dom ((f * F) /. x) by A2, Def6

.= (doms (f * F)) /. x by A2, Def1 ; :: thesis: verum

end;assume A2: x in I ; :: thesis: (doms F) /. x = (doms (f * F)) /. x

then A3: cod (F /. x) = (I --> (dom f)) /. x by A1, Def2

.= dom f by A2, Th2 ;

thus (doms F) /. x = dom (F /. x) by A2, Def1

.= dom (f (*) (F /. x)) by A3, CAT_1:17

.= dom ((f * F) /. x) by A2, Def6

.= (doms (f * F)) /. x by A2, Def1 ; :: thesis: verum

now :: thesis: for x being set st x in I holds

(cods (f * F)) /. x = (I --> (cod f)) /. x

hence
cods (f * F) = I --> (cod f)
by Th1; :: thesis: verum(cods (f * F)) /. x = (I --> (cod f)) /. x

let x be set ; :: thesis: ( x in I implies (cods (f * F)) /. x = (I --> (cod f)) /. x )

assume A4: x in I ; :: thesis: (cods (f * F)) /. x = (I --> (cod f)) /. x

then A5: cod (F /. x) = (I --> (dom f)) /. x by A1, Def2

.= dom f by A4, Th2 ;

thus (cods (f * F)) /. x = cod ((f * F) /. x) by A4, Def2

.= cod (f (*) (F /. x)) by A4, Def6

.= cod f by A5, CAT_1:17

.= (I --> (cod f)) /. x by A4, Th2 ; :: thesis: verum

end;assume A4: x in I ; :: thesis: (cods (f * F)) /. x = (I --> (cod f)) /. x

then A5: cod (F /. x) = (I --> (dom f)) /. x by A1, Def2

.= dom f by A4, Th2 ;

thus (cods (f * F)) /. x = cod ((f * F) /. x) by A4, Def2

.= cod (f (*) (F /. x)) by A4, Def6

.= cod f by A5, CAT_1:17

.= (I --> (cod f)) /. x by A4, Th2 ; :: thesis: verum