thus ( P is coprojection-morphisms implies for Y being Object of C
for F being MorphismsFamily of A,Y st F is feasible holds
ex f being Morphism of B,Y st
( f in <^B,Y^> & ( for i being Element of I holds F . i = f * (P . i) ) & ( for f1 being Morphism of B,Y st ( for i being Element of I holds F . i = f1 * (P . i) ) holds
f = f1 ) ) ) :: thesis:

proof

assume A1: P is coprojection-morphisms ; :: thesis:
let Y be Object of C; :: thesis:
let F be MorphismsFamily of A,Y; :: thesis:
assume A2: F is feasible ; :: thesis:
consider f being Morphism of B,Y such that
A3: f in <^B,Y^> and
A4: for i being set st i in I holds
ex si being Object of C ex Pi being Morphism of si,B st
( si = A . i & Pi = P . i & F . i = f * Pi ) and
A5: for f1 being Morphism of B,Y st ( for i being set st i in I holds
ex si being Object of C ex Pi being Morphism of si,B st
( si = A . i & Pi = P . i & F . i = f1 * Pi ) ) holds
f = f1 by A2, A1;
take f ; :: thesis:
thus f in <^B,Y^> by A3; :: thesis:

hereby :: thesis:

let i be Element of I; :: thesis:
ex si being Object of C ex Pi being Morphism of si,B st
( si = A . i & Pi = P . i & F . i = f * Pi ) by A4;
hence F . i = f * (P . i) ; :: thesis:

end;

let f1 be Morphism of B,Y; :: thesis:
assume A6: for i being Element of I holds F . i = f1 * (P . i) ; :: thesis:
for i being set st i in I holds
ex si being Object of C ex Pi being Morphism of si,B st
( si = A . i & Pi = P . i & F . i = f1 * Pi )

proof

let i be set ; :: thesis:
assume i in I ; :: thesis:
then reconsider i = i as Element of I ;
reconsider si = A . i as Object of C ;
reconsider Pi = P . i as Morphism of si,B ;
take si ; :: thesis:
take Pi ; :: thesis:
thus ( si = A . i & Pi = P . i & F . i = f1 * Pi ) by A6; :: thesis:

end;

hence f = f1 by A5; :: thesis:

end;

assume A7: for Y being Object of C
for F being MorphismsFamily of A,Y st F is feasible holds
ex f being Morphism of B,Y st
( f in <^B,Y^> & ( for i being Element of I holds F . i = f * (P . i) ) & ( for f1 being Morphism of B,Y st ( for i being Element of I holds F . i = f1 * (P . i) ) holds
f = f1 ) ) ; :: thesis:
let Y be Object of C; :: according to ALTCAT_6:def 5 :: thesis:
let F be MorphismsFamily of A,Y; :: thesis:
assume F is feasible ; :: thesis:
then consider f being Morphism of B,Y such that
A8: f in <^B,Y^> and
A9: for i being Element of I holds F . i = f * (P . i) and
A10: for f1 being Morphism of B,Y st ( for i being Element of I holds F . i = f1 * (P . i) ) holds
f = f1 by A7;
take f ; :: thesis:
thus f in <^B,Y^> by A8; :: thesis:
thus for i being set st i in I holds
ex si being Object of C ex Pi being Morphism of si,B st
( si = A . i & Pi = P . i & F . i = f * Pi ) :: thesis:

proof

let i be set ; :: thesis:
assume i in I ; :: thesis:
then reconsider j = i as Element of I ;
take A . j ; :: thesis:
take P . j ; :: thesis:
thus ( A . j = A . i & P . j = P . i & F . i = f * (P . j) ) by A9; :: thesis:

end;

let f1 be Morphism of B,Y; :: thesis:
assume A11: for i being set st i in I holds
ex si being Object of C ex Pi being Morphism of si,B st
( si = A . i & Pi = P . i & F . i = f1 * Pi ) ; :: thesis:

now :: thesis:

let i be Element of I; :: thesis:
ex si being Object of C ex Pi being Morphism of si,B st
( si = A . i & Pi = P . i & F . i = f1 * Pi ) by A11;
hence F . i = f1 * (P . i) ; :: thesis:

end;

hence f = f1 by A10; :: thesis: