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

proof

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

hereby :: thesis:

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

end;

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

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 B,si ;
take si ; :: thesis:
take Pi ; :: thesis:
thus ( si = A . i & Pi = P . i & F . i = Pi * f1 ) by A6; :: thesis:

end;

hence f = f1 by A5; :: thesis:

end;

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

end;

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

now :: thesis:

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

end;

hence f = f1 by A10; :: thesis: