let I be set ; :: thesis: for C being category
for A being ObjectsFamily of I,C
for C1, C2 being Object of C st C1 is A -CatCoproduct-like & C2 is A -CatCoproduct-like holds
C1,C2 are_iso
let C be category; :: thesis: for A being ObjectsFamily of I,C
for C1, C2 being Object of C st C1 is A -CatCoproduct-like & C2 is A -CatCoproduct-like holds
C1,C2 are_iso
let A be ObjectsFamily of I,C; :: thesis: for C1, C2 being Object of C st C1 is A -CatCoproduct-like & C2 is A -CatCoproduct-like holds
C1,C2 are_iso
let C1, C2 be Object of C; :: thesis: ( C1 is A -CatCoproduct-like & C2 is A -CatCoproduct-like implies C1,C2 are_iso )
assume that
A1: C1 is A -CatCoproduct-like and
A2: C2 is A -CatCoproduct-like ; :: thesis: C1,C2 are_iso

per cases ( I is empty or not I is empty ) ;

suppose I is empty ; :: thesis: C1,C2 are_iso

hence C1,C2 are_iso by A1, A2, ALTCAT_3:26; :: thesis: verum

end;

suppose not I is empty ; :: thesis: C1,C2 are_iso

then reconsider I = I as non empty set ;
reconsider A = A as ObjectsFamily of I,C ;
consider P1 being MorphismsFamily of A,C1 such that
A3: P1 is feasible and
A4: P1 is coprojection-morphisms by A1;
consider P2 being MorphismsFamily of A,C2 such that
A5: P2 is feasible and
A6: P2 is coprojection-morphisms by A2;
consider f1 being Morphism of C1,C2 such that
A7: f1 in <^C1,C2^> and
A8: for i being Element of I holds P2 . i = f1 * (P1 . i) and
for fa being Morphism of C1,C2 st ( for i being Element of I holds P2 . i = fa * (P1 . i) ) holds
f1 = fa by A4, A5;
consider g1 being Morphism of C1,C1 such that
g1 in <^C1,C1^> and
for i being Element of I holds P1 . i = g1 * (P1 . i) and
A9: for fa being Morphism of C1,C1 st ( for i being Element of I holds P1 . i = fa * (P1 . i) ) holds
g1 = fa by A3, A4;
consider f2 being Morphism of C2,C1 such that
A10: f2 in <^C2,C1^> and
A11: for i being Element of I holds P1 . i = f2 * (P2 . i) and
for fa being Morphism of C2,C1 st ( for i being Element of I holds P1 . i = fa * (P2 . i) ) holds
f2 = fa by A3, A6;
consider g2 being Morphism of C2,C2 such that
g2 in <^C2,C2^> and
for i being Element of I holds P2 . i = g2 * (P2 . i) and
A12: for fa being Morphism of C2,C2 st ( for i being Element of I holds P2 . i = fa * (P2 . i) ) holds
fa = g2 by A5, A6;
thus ( <^C1,C2^> <> {} & <^C2,C1^> <> {} ) by A7, A10; :: according to ALTCAT_3:def 6 :: thesis: ex b₁ being Element of <^C1,C2^> st b₁ is iso
take f1 ; :: thesis: f1 is iso
A13: f1 is retraction

proof

take f2 ; :: according to ALTCAT_3:def 2 :: thesis: f1 is_left_inverse_of f2

now :: thesis: for i being Element of I holds P2 . i = (idm C2) * (P2 . i)

let i be Element of I; :: thesis: P2 . i = (idm C2) * (P2 . i)
P2 . i in <^(A . i),C2^> by A5;
hence P2 . i = (idm C2) * (P2 . i) by ALTCAT_1:20; :: thesis: verum

end;

then A14: g2 = idm C2 by A12;

now :: thesis: for i being Element of I holds (f1 * f2) * (P2 . i) = P2 . i

let i be Element of I; :: thesis: (f1 * f2) * (P2 . i) = P2 . i
P2 . i in <^(A . i),C2^> by A5;
hence (f1 * f2) * (P2 . i) = f1 * (f2 * (P2 . i)) by A7, A10, ALTCAT_1:21
.= f1 * (P1 . i) by A11
.= P2 . i by A8 ;
:: thesis: verum

end;

hence f1 * f2 = idm C2 by A14, A12; :: according to ALTCAT_3:def 1 :: thesis: verum

end;

f1 is coretraction

proof

take f2 ; :: according to ALTCAT_3:def 3 :: thesis: f2 is_left_inverse_of f1

now :: thesis: for i being Element of I holds P1 . i = (idm C1) * (P1 . i)

let i be Element of I; :: thesis: P1 . i = (idm C1) * (P1 . i)
P1 . i in <^(A . i),C1^> by A3;
hence P1 . i = (idm C1) * (P1 . i) by ALTCAT_1:20; :: thesis: verum

end;

then A15: g1 = idm C1 by A9;

now :: thesis: for i being Element of I holds (f2 * f1) * (P1 . i) = P1 . i

let i be Element of I; :: thesis: (f2 * f1) * (P1 . i) = P1 . i
P1 . i in <^(A . i),C1^> by A3;
hence (f2 * f1) * (P1 . i) = f2 * (f1 * (P1 . i)) by A7, A10, ALTCAT_1:21
.= f2 * (P2 . i) by A8
.= P1 . i by A11 ;
:: thesis: verum

end;

hence f2 * f1 = idm C1 by A15, A9; :: according to ALTCAT_3:def 1 :: thesis: verum

end;

hence f1 is iso by A7, A10, A13, ALTCAT_3:6; :: thesis: verum

end;

end;