let I be set ; :: thesis: for C being Category

for F, G being Function of I, the carrier' of C st doms F = cods G holds

( doms (F "*" G) = doms G & cods (F "*" G) = cods F )

let C be Category; :: thesis: for F, G being Function of I, the carrier' of C st doms F = cods G holds

( doms (F "*" G) = doms G & cods (F "*" G) = cods F )

let F, G be Function of I, the carrier' of C; :: thesis: ( doms F = cods G implies ( doms (F "*" G) = doms G & cods (F "*" G) = cods F ) )

assume A1: doms F = cods G ; :: thesis: ( doms (F "*" G) = doms G & cods (F "*" G) = cods F )

for F, G being Function of I, the carrier' of C st doms F = cods G holds

( doms (F "*" G) = doms G & cods (F "*" G) = cods F )

let C be Category; :: thesis: for F, G being Function of I, the carrier' of C st doms F = cods G holds

( doms (F "*" G) = doms G & cods (F "*" G) = cods F )

let F, G be Function of I, the carrier' of C; :: thesis: ( doms F = cods G implies ( doms (F "*" G) = doms G & cods (F "*" G) = cods F ) )

assume A1: doms F = cods G ; :: thesis: ( doms (F "*" G) = doms G & cods (F "*" G) = cods F )

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

(doms (F "*" G)) /. x = (doms G) /. x

hence
doms (F "*" G) = doms G
by Th1; :: thesis: cods (F "*" G) = cods F(doms (F "*" G)) /. x = (doms G) /. x

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

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

then A3: cod (G /. x) = (doms F) /. x by A1, Def2

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

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

.= dom ((F /. x) (*) (G /. x)) by A2, Def7

.= dom (G /. x) by A3, CAT_1:17

.= (doms G) /. x by A2, Def1 ; :: thesis: verum

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

then A3: cod (G /. x) = (doms F) /. x by A1, Def2

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

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

.= dom ((F /. x) (*) (G /. x)) by A2, Def7

.= dom (G /. x) by A3, CAT_1:17

.= (doms G) /. x by A2, Def1 ; :: thesis: verum

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

(cods (F "*" G)) /. x = (cods F) /. x

hence
cods (F "*" G) = cods F
by Th1; :: thesis: verum(cods (F "*" G)) /. x = (cods F) /. x

let x be set ; :: thesis: ( x in I implies (cods (F "*" G)) /. x = (cods F) /. x )

assume A4: x in I ; :: thesis: (cods (F "*" G)) /. x = (cods F) /. x

then A5: cod (G /. x) = (doms F) /. x by A1, Def2

.= dom (F /. x) by A4, Def1 ;

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

.= cod ((F /. x) (*) (G /. x)) by A4, Def7

.= cod (F /. x) by A5, CAT_1:17

.= (cods F) /. x by A4, Def2 ; :: thesis: verum

end;assume A4: x in I ; :: thesis: (cods (F "*" G)) /. x = (cods F) /. x

then A5: cod (G /. x) = (doms F) /. x by A1, Def2

.= dom (F /. x) by A4, Def1 ;

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

.= cod ((F /. x) (*) (G /. x)) by A4, Def7

.= cod (F /. x) by A5, CAT_1:17

.= (cods F) /. x by A4, Def2 ; :: thesis: verum