let C be category; :: thesis:
let c1, c2, c3, c4, c5, c6 be Object of C; :: thesis:
let f1 be Morphism of c1,c2; :: thesis:
let f2 be Morphism of c2,c3; :: thesis:
let f3 be Morphism of c1,c4; :: thesis:
let f4 be Morphism of c2,c5; :: thesis:
let f5 be Morphism of c3,c6; :: thesis:
let f6 be Morphism of c4,c5; :: thesis:
let f7 be Morphism of c5,c6; :: thesis:
assume A1: ( Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} ) ; :: thesis:
assume A2: c2,f2,f4 is_pullback_of f5,f7 ; :: thesis:
then A3: ( f5 * f2 = f7 * f4 & ( for d1 being Object of C
for g1 being Morphism of d1,c3
for g2 being Morphism of d1,c5 st Hom (d1,c3) <> {} & Hom (d1,c5) <> {} & f5 * g1 = f7 * g2 holds
( Hom (d1,c2) <> {} & ex h being Morphism of d1,c2 st
( f2 * h = g1 & f4 * h = g2 & ( for h1 being Morphism of d1,c2 st f2 * h1 = g1 & f4 * h1 = g2 holds
h = h1 ) ) ) ) ) by A1, Def17;

hereby :: thesis:

assume A4: c1,f1,f3 is_pullback_of f4,f6 ; :: thesis:
then A5: ( f4 * f1 = f6 * f3 & ( for d1 being Object of C
for g1 being Morphism of d1,c2
for g2 being Morphism of d1,c4 st Hom (d1,c2) <> {} & Hom (d1,c4) <> {} & f4 * g1 = f6 * g2 holds
( Hom (d1,c1) <> {} & ex h being Morphism of d1,c1 st
( f1 * h = g1 & f3 * h = g2 & ( for h1 being Morphism of d1,c1 st f1 * h1 = g1 & f3 * h1 = g2 holds
h = h1 ) ) ) ) ) by A1, Def17;
A6: ( Hom (c4,c6) <> {} & Hom (c1,c3) <> {} & Hom (c1,c4) <> {} ) by A1, Th22;
A7: f5 * (f2 * f1) = (f5 * f2) * f1 by A1, Th23
.= f7 * (f6 * f3) by A3, A5, Th23, A1
.= (f7 * f6) * f3 by A1, Th23 ;
for d1 being Object of C
for g1 being Morphism of d1,c3
for g2 being Morphism of d1,c4 st Hom (d1,c3) <> {} & Hom (d1,c4) <> {} & f5 * g1 = (f7 * f6) * g2 holds
( Hom (d1,c1) <> {} & ex h being Morphism of d1,c1 st
( (f2 * f1) * h = g1 & f3 * h = g2 & ( for h1 being Morphism of d1,c1 st (f2 * f1) * h1 = g1 & f3 * h1 = g2 holds
h = h1 ) ) )

proof

let d1 be Object of C; :: thesis:
let g1 be Morphism of d1,c3; :: thesis:
let g2 be Morphism of d1,c4; :: thesis:
assume A8: Hom (d1,c3) <> {} ; :: thesis:
assume A9: Hom (d1,c4) <> {} ; :: thesis:
assume A10: f5 * g1 = (f7 * f6) * g2 ; :: thesis:
A11: Hom (d1,c5) <> {} by A9, A1, Th22;
A12: f5 * g1 = f7 * (f6 * g2) by A10, A9, A1, Th23;
then A13: ( Hom (d1,c2) <> {} & ex h being Morphism of d1,c2 st
( f2 * h = g1 & f4 * h = f6 * g2 & ( for h1 being Morphism of d1,c2 st f2 * h1 = g1 & f4 * h1 = f6 * g2 holds
h = h1 ) ) ) by A1, A2, A11, A8, Def17;
consider g3 being Morphism of d1,c2 such that
A14: ( f2 * g3 = g1 & f4 * g3 = f6 * g2 & ( for h1 being Morphism of d1,c2 st f2 * h1 = g1 & f4 * h1 = f6 * g2 holds
g3 = h1 ) ) by A1, A12, A2, A11, A8, Def17;
thus A15: Hom (d1,c1) <> {} by A1, A13, A9, A4, Def17; :: thesis:
consider h being Morphism of d1,c1 such that
A16: ( f1 * h = g3 & f3 * h = g2 & ( for h1 being Morphism of d1,c1 st f1 * h1 = g3 & f3 * h1 = g2 holds
h = h1 ) ) by A1, A14, A13, A9, A4, Def17;
take h ; :: thesis:
thus (f2 * f1) * h = g1 by A1, A14, A16, A15, Th23; :: thesis:
thus f3 * h = g2 by A16; :: thesis:
let h1 be Morphism of d1,c1; :: thesis:
assume A17: (f2 * f1) * h1 = g1 ; :: thesis:
assume A18: f3 * h1 = g2 ; :: thesis:
A19: f2 * (f1 * h1) = g1 by A1, A17, A15, Th23;
f4 * (f1 * h1) = (f4 * f1) * h1 by A1, A15, Th23
.= f6 * g2 by A18, A5, A15, Th23, A1 ;
then g3 = f1 * h1 by A19, A14;
hence h = h1 by A18, A16; :: thesis:

end;

hence c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 by A1, A6, A7, Def17; :: thesis:
thus f4 * f1 = f6 * f3 by A1, A4, Def17; :: thesis:

end;

A20: ( Hom (c1,c3) <> {} & Hom (c3,c6) <> {} & Hom (c4,c6) <> {} ) by A1, Th22;
assume A21: c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 ; :: thesis:
assume A22: f4 * f1 = f6 * f3 ; :: thesis:
for d1 being Object of C
for g1 being Morphism of d1,c2
for g2 being Morphism of d1,c4 st Hom (d1,c2) <> {} & Hom (d1,c4) <> {} & f4 * g1 = f6 * g2 holds
( Hom (d1,c1) <> {} & ex h being Morphism of d1,c1 st
( f1 * h = g1 & f3 * h = g2 & ( for h1 being Morphism of d1,c1 st f1 * h1 = g1 & f3 * h1 = g2 holds
h = h1 ) ) )

proof

let d1 be Object of C; :: thesis:
let g1 be Morphism of d1,c2; :: thesis:
let g2 be Morphism of d1,c4; :: thesis:
assume A23: Hom (d1,c2) <> {} ; :: thesis:
assume A24: Hom (d1,c4) <> {} ; :: thesis:
assume A25: f4 * g1 = f6 * g2 ; :: thesis:
set g11 = f2 * g1;
A26: Hom (d1,c3) <> {} by A1, A23, Th22;
A27: f5 * (f2 * g1) = (f5 * f2) * g1 by A23, A1, Th23
.= f7 * (f6 * g2) by A25, A23, A3, Th23, A1
.= (f7 * f6) * g2 by A24, A1, Th23 ;
then A28: ( Hom (d1,c1) <> {} & ex h being Morphism of d1,c1 st
( (f2 * f1) * h = f2 * g1 & f3 * h = g2 & ( for h1 being Morphism of d1,c1 st (f2 * f1) * h1 = f2 * g1 & f3 * h1 = g2 holds
h = h1 ) ) ) by A1, A24, A26, A21, A20, Def17;
thus A29: Hom (d1,c1) <> {} by A1, A27, A24, A26, A21, A20, Def17; :: thesis:
consider h being Morphism of d1,c1 such that
A30: ( (f2 * f1) * h = f2 * g1 & f3 * h = g2 & ( for h1 being Morphism of d1,c1 st (f2 * f1) * h1 = f2 * g1 & f3 * h1 = g2 holds
h = h1 ) ) by A1, A27, A24, A26, A21, A20, Def17;
take h ; :: thesis:
set g22 = f4 * g1;
A31: ( Hom (d1,c3) <> {} & Hom (d1,c5) <> {} ) by A1, A23, Th22;
A32: f5 * (f2 * g1) = (f5 * f2) * g1 by A23, A1, Th23
.= f7 * (f4 * g1) by A23, A3, Th23, A1 ;
consider h2 being Morphism of d1,c2 such that
A33: ( f2 * h2 = f2 * g1 & f4 * h2 = f4 * g1 & ( for h1 being Morphism of d1,c2 st f2 * h1 = f2 * g1 & f4 * h1 = f4 * g1 holds
h2 = h1 ) ) by A1, A32, A31, A2, Def17;
A34: h2 = g1 by A33;
A35: f2 * (f1 * h) = f2 * g1 by A1, A30, A28, Th23;
f4 * (f1 * h) = (f4 * f1) * h by A1, A28, Th23
.= f4 * g1 by A30, A25, A22, A28, A1, Th23 ;
hence f1 * h = g1 by A33, A35, A34; :: thesis:
thus f3 * h = g2 by A30; :: thesis:
let h1 be Morphism of d1,c1; :: thesis:
assume A36: f1 * h1 = g1 ; :: thesis:
A37: (f2 * f1) * h1 = f2 * g1 by A1, A36, A29, Th23;
assume f3 * h1 = g2 ; :: thesis:
hence h = h1 by A30, A37; :: thesis:

end;

hence c1,f1,f3 is_pullback_of f4,f6 by A22, A1, Def17; :: thesis: