let I be set ; :: thesis: for C being Category
for a, b being Object of C
for f being Morphism of C
for F being Projections_family of a,I st a is_a_product_wrt F & dom f = b & cod f = a & f is invertible holds
b is_a_product_wrt F * f
let C be Category; :: thesis: for a, b being Object of C
for f being Morphism of C
for F being Projections_family of a,I st a is_a_product_wrt F & dom f = b & cod f = a & f is invertible holds
b is_a_product_wrt F * f
let a, b be Object of C; :: thesis: for f being Morphism of C
for F being Projections_family of a,I st a is_a_product_wrt F & dom f = b & cod f = a & f is invertible holds
b is_a_product_wrt F * f
let f be Morphism of C; :: thesis: for F being Projections_family of a,I st a is_a_product_wrt F & dom f = b & cod f = a & f is invertible holds
b is_a_product_wrt F * f
let F be Projections_family of a,I; :: thesis: ( a is_a_product_wrt F & dom f = b & cod f = a & f is invertible implies b is_a_product_wrt F * f )
assume that
A1: a is_a_product_wrt F and
A2: dom f = b and
A3: cod f = a and
A4: f is invertible ; :: thesis: b is_a_product_wrt F * f
thus F * f is Projections_family of b,I by A2, A3, Th50; :: according to CAT_3:def 13 :: thesis: for b being Object of C
for F9 being Projections_family of b,I st cods (F * f) = cods F9 holds
ex h being Morphism of C st
( h in Hom (b,b) & ( for k being Morphism of C st k in Hom (b,b) holds
( ( for x being set st x in I holds
((F * f) /. x) * k = F9 /. x ) iff h = k ) ) )
let c be Object of C; :: thesis: for F9 being Projections_family of c,I st cods (F * f) = cods F9 holds
ex h being Morphism of C st
( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in I holds
((F * f) /. x) * k = F9 /. x ) iff h = k ) ) )
A5: doms F = I --> (cod f) by A3, Def14;
let F9 be Projections_family of c,I; :: thesis: ( cods (F * f) = cods F9 implies ex h being Morphism of C st
( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in I holds
((F * f) /. x) * k = F9 /. x ) iff h = k ) ) ) )
assume cods (F * f) = cods F9 ; :: thesis: ex h being Morphism of C st
( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in I holds
((F * f) /. x) * k = F9 /. x ) iff h = k ) ) )
then cods F = cods F9 by A5, Th20;
then consider h being Morphism of C such that
A6: h in Hom (c,a) and
A7: for k being Morphism of C st k in Hom (c,a) holds
( ( for x being set st x in I holds
(F /. x) * k = F9 /. x ) iff h = k ) by A1, Def15;
A8: cod h = a by A6, CAT_1:1;
consider g being Morphism of C such that
A9: dom g = cod f and
A10: cod g = dom f and
A11: f * g = id (cod f) and
A12: g * f = id (dom f) by A4, CAT_1:def 9;
dom h = c by A6, CAT_1:1;
then A13: dom (g * h) = c by A3, A9, A8, CAT_1:17;
take gh = g * h; :: thesis: ( gh in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in I holds
((F * f) /. x) * k = F9 /. x ) iff gh = k ) ) )
cod (g * h) = b by A2, A3, A9, A10, A8, CAT_1:17;
hence gh in Hom (c,b) by A13; :: thesis: for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in I holds
((F * f) /. x) * k = F9 /. x ) iff gh = k )
let k be Morphism of C; :: thesis: ( k in Hom (c,b) implies ( ( for x being set st x in I holds
((F * f) /. x) * k = F9 /. x ) iff gh = k ) )
assume A14: k in Hom (c,b) ; :: thesis: ( ( for x being set st x in I holds
((F * f) /. x) * k = F9 /. x ) iff gh = k )
then A15: cod k = b by CAT_1:1;
A16: dom k = c by A14, CAT_1:1;
thus ( ( for x being set st x in I holds
((F * f) /. x) * k = F9 /. x ) implies gh = k ) :: thesis: ( gh = k implies for x being set st x in I holds
((F * f) /. x) * k = F9 /. x )

proof

assume A17: for x being set st x in I holds
((F * f) /. x) * k = F9 /. x ; :: thesis: gh = k

now

( dom (f * k) = c & cod (f * k) = a ) by A2, A3, A16, A15, CAT_1:17;
hence f * k in Hom (c,a) ; :: thesis: for x being set st x in I holds
(F /. x) * (f * k) = F9 /. x
let x be set ; :: thesis: ( x in I implies (F /. x) * (f * k) = F9 /. x )
assume A18: x in I ; :: thesis: (F /. x) * (f * k) = F9 /. x
then dom (F /. x) = a by Th45;
hence (F /. x) * (f * k) = ((F /. x) * f) * k by A2, A3, A15, CAT_1:18
.= ((F * f) /. x) * k by A18, Def7
.= F9 /. x by A17, A18 ;
:: thesis: verum

end;

then g * (f * k) = g * h by A7;
hence gh = (id b) * k by A2, A9, A12, A15, CAT_1:18
.= k by A15, CAT_1:21 ;
:: thesis: verum

end;

assume A19: gh = k ; :: thesis: for x being set st x in I holds
((F * f) /. x) * k = F9 /. x
let x be set ; :: thesis: ( x in I implies ((F * f) /. x) * k = F9 /. x )
assume A20: x in I ; :: thesis: ((F * f) /. x) * k = F9 /. x
then A21: dom (F /. x) = a by Th45;
thus ((F * f) /. x) * k = ((F /. x) * f) * k by A20, Def7
.= (F /. x) * (f * (g * h)) by A2, A3, A15, A19, A21, CAT_1:18
.= (F /. x) * ((id (cod f)) * h) by A3, A9, A10, A11, A8, CAT_1:18
.= (F /. x) * h by A3, A8, CAT_1:21
.= F9 /. x by A6, A7, A20 ; :: thesis: verum