let C be category; :: thesis: for c1, c2, c3, c4, c5, c6 being Object of C

for f1 being Morphism of c1,c2

for f2 being Morphism of c2,c3

for f3 being Morphism of c1,c4

for f4 being Morphism of c2,c5

for f5 being Morphism of c3,c6

for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let c1, c2, c3, c4, c5, c6 be Object of C; :: thesis: for f1 being Morphism of c1,c2

for f2 being Morphism of c2,c3

for f3 being Morphism of c1,c4

for f4 being Morphism of c2,c5

for f5 being Morphism of c3,c6

for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let f1 be Morphism of c1,c2; :: thesis: for f2 being Morphism of c2,c3

for f3 being Morphism of c1,c4

for f4 being Morphism of c2,c5

for f5 being Morphism of c3,c6

for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let f2 be Morphism of c2,c3; :: thesis: for f3 being Morphism of c1,c4

for f4 being Morphism of c2,c5

for f5 being Morphism of c3,c6

for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let f3 be Morphism of c1,c4; :: thesis: for f4 being Morphism of c2,c5

for f5 being Morphism of c3,c6

for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let f4 be Morphism of c2,c5; :: thesis: for f5 being Morphism of c3,c6

for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let f5 be Morphism of c3,c6; :: thesis: for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let f6 be Morphism of c4,c5; :: thesis: for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let f7 be Morphism of c5,c6; :: thesis: ( Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 implies ( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) ) )

assume A1: ( Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} ) ; :: thesis: ( not c2,f2,f4 is_pullback_of f5,f7 or ( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) ) )

assume A2: c2,f2,f4 is_pullback_of f5,f7 ; :: thesis: ( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

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;

assume A21: c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 ; :: thesis: ( not f4 * f1 = f6 * f3 or c1,f1,f3 is_pullback_of f4,f6 )

assume A22: f4 * f1 = f6 * f3 ; :: thesis: c1,f1,f3 is_pullback_of f4,f6

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 ) ) )

for f1 being Morphism of c1,c2

for f2 being Morphism of c2,c3

for f3 being Morphism of c1,c4

for f4 being Morphism of c2,c5

for f5 being Morphism of c3,c6

for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let c1, c2, c3, c4, c5, c6 be Object of C; :: thesis: for f1 being Morphism of c1,c2

for f2 being Morphism of c2,c3

for f3 being Morphism of c1,c4

for f4 being Morphism of c2,c5

for f5 being Morphism of c3,c6

for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let f1 be Morphism of c1,c2; :: thesis: for f2 being Morphism of c2,c3

for f3 being Morphism of c1,c4

for f4 being Morphism of c2,c5

for f5 being Morphism of c3,c6

for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let f2 be Morphism of c2,c3; :: thesis: for f3 being Morphism of c1,c4

for f4 being Morphism of c2,c5

for f5 being Morphism of c3,c6

for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let f3 be Morphism of c1,c4; :: thesis: for f4 being Morphism of c2,c5

for f5 being Morphism of c3,c6

for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let f4 be Morphism of c2,c5; :: thesis: for f5 being Morphism of c3,c6

for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let f5 be Morphism of c3,c6; :: thesis: for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let f6 be Morphism of c4,c5; :: thesis: for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

let f7 be Morphism of c5,c6; :: thesis: ( Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 implies ( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) ) )

assume A1: ( Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} ) ; :: thesis: ( not c2,f2,f4 is_pullback_of f5,f7 or ( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) ) )

assume A2: c2,f2,f4 is_pullback_of f5,f7 ; :: thesis: ( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

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: ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 implies c1,f1,f3 is_pullback_of f4,f6 )

A20:
( Hom (c1,c3) <> {} & Hom (c3,c6) <> {} & Hom (c4,c6) <> {} )
by A1, Th22;assume A4:
c1,f1,f3 is_pullback_of f4,f6
; :: thesis: ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 )

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 ) ) )

thus f4 * f1 = f6 * f3 by A1, A4, Def17; :: thesis: verum

end;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

hence
c1,f2 * f1,f3 is_pullback_of f5,f7 * f6
by A1, A6, A7, Def17; :: thesis: f4 * f1 = f6 * f3
let d1 be Object of C; :: thesis: 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 ) ) )

let g1 be Morphism of d1,c3; :: thesis: 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 ) ) )

let g2 be Morphism of d1,c4; :: thesis: ( Hom (d1,c3) <> {} & Hom (d1,c4) <> {} & f5 * g1 = (f7 * f6) * g2 implies ( 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 ) ) ) )

assume A8: Hom (d1,c3) <> {} ; :: thesis: ( not Hom (d1,c4) <> {} or not f5 * g1 = (f7 * f6) * g2 or ( 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 ) ) ) )

assume A9: Hom (d1,c4) <> {} ; :: thesis: ( not f5 * g1 = (f7 * f6) * g2 or ( 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 ) ) ) )

assume A10: f5 * g1 = (f7 * f6) * g2 ; :: thesis: ( 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 ) ) )

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: 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 ) )

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: ( (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 ) )

thus (f2 * f1) * h = g1 by A1, A14, A16, A15, Th23; :: thesis: ( f3 * h = g2 & ( for h1 being Morphism of d1,c1 st (f2 * f1) * h1 = g1 & f3 * h1 = g2 holds

h = h1 ) )

thus f3 * h = g2 by A16; :: thesis: for h1 being Morphism of d1,c1 st (f2 * f1) * h1 = g1 & f3 * h1 = g2 holds

h = h1

let h1 be Morphism of d1,c1; :: thesis: ( (f2 * f1) * h1 = g1 & f3 * h1 = g2 implies h = h1 )

assume A17: (f2 * f1) * h1 = g1 ; :: thesis: ( not f3 * h1 = g2 or h = h1 )

assume A18: f3 * h1 = g2 ; :: thesis: h = h1

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: verum

end;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 ) ) )

let g1 be Morphism of d1,c3; :: thesis: 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 ) ) )

let g2 be Morphism of d1,c4; :: thesis: ( Hom (d1,c3) <> {} & Hom (d1,c4) <> {} & f5 * g1 = (f7 * f6) * g2 implies ( 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 ) ) ) )

assume A8: Hom (d1,c3) <> {} ; :: thesis: ( not Hom (d1,c4) <> {} or not f5 * g1 = (f7 * f6) * g2 or ( 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 ) ) ) )

assume A9: Hom (d1,c4) <> {} ; :: thesis: ( not f5 * g1 = (f7 * f6) * g2 or ( 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 ) ) ) )

assume A10: f5 * g1 = (f7 * f6) * g2 ; :: thesis: ( 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 ) ) )

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: 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 ) )

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: ( (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 ) )

thus (f2 * f1) * h = g1 by A1, A14, A16, A15, Th23; :: thesis: ( f3 * h = g2 & ( for h1 being Morphism of d1,c1 st (f2 * f1) * h1 = g1 & f3 * h1 = g2 holds

h = h1 ) )

thus f3 * h = g2 by A16; :: thesis: for h1 being Morphism of d1,c1 st (f2 * f1) * h1 = g1 & f3 * h1 = g2 holds

h = h1

let h1 be Morphism of d1,c1; :: thesis: ( (f2 * f1) * h1 = g1 & f3 * h1 = g2 implies h = h1 )

assume A17: (f2 * f1) * h1 = g1 ; :: thesis: ( not f3 * h1 = g2 or h = h1 )

assume A18: f3 * h1 = g2 ; :: thesis: h = h1

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: verum

thus f4 * f1 = f6 * f3 by A1, A4, Def17; :: thesis: verum

assume A21: c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 ; :: thesis: ( not f4 * f1 = f6 * f3 or c1,f1,f3 is_pullback_of f4,f6 )

assume A22: f4 * f1 = f6 * f3 ; :: thesis: c1,f1,f3 is_pullback_of f4,f6

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

hence
c1,f1,f3 is_pullback_of f4,f6
by A22, A1, Def17; :: thesis: verum
let d1 be Object of C; :: thesis: 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 ) ) )

let g1 be Morphism of d1,c2; :: thesis: 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 ) ) )

let g2 be Morphism of d1,c4; :: thesis: ( Hom (d1,c2) <> {} & Hom (d1,c4) <> {} & f4 * g1 = f6 * g2 implies ( 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 ) ) ) )

assume A23: Hom (d1,c2) <> {} ; :: thesis: ( not Hom (d1,c4) <> {} or not f4 * g1 = f6 * g2 or ( 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 ) ) ) )

assume A24: Hom (d1,c4) <> {} ; :: thesis: ( not f4 * g1 = f6 * g2 or ( 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 ) ) ) )

assume A25: f4 * g1 = f6 * g2 ; :: thesis: ( 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 ) ) )

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: 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 ) )

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: ( f1 * h = g1 & f3 * h = g2 & ( for h1 being Morphism of d1,c1 st f1 * h1 = g1 & f3 * h1 = g2 holds

h = h1 ) )

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: ( f3 * h = g2 & ( for h1 being Morphism of d1,c1 st f1 * h1 = g1 & f3 * h1 = g2 holds

h = h1 ) )

thus f3 * h = g2 by A30; :: thesis: for h1 being Morphism of d1,c1 st f1 * h1 = g1 & f3 * h1 = g2 holds

h = h1

let h1 be Morphism of d1,c1; :: thesis: ( f1 * h1 = g1 & f3 * h1 = g2 implies h = h1 )

assume A36: f1 * h1 = g1 ; :: thesis: ( not f3 * h1 = g2 or h = h1 )

A37: (f2 * f1) * h1 = f2 * g1 by A1, A36, A29, Th23;

assume f3 * h1 = g2 ; :: thesis: h = h1

hence h = h1 by A30, A37; :: thesis: verum

end;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 ) ) )

let g1 be Morphism of d1,c2; :: thesis: 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 ) ) )

let g2 be Morphism of d1,c4; :: thesis: ( Hom (d1,c2) <> {} & Hom (d1,c4) <> {} & f4 * g1 = f6 * g2 implies ( 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 ) ) ) )

assume A23: Hom (d1,c2) <> {} ; :: thesis: ( not Hom (d1,c4) <> {} or not f4 * g1 = f6 * g2 or ( 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 ) ) ) )

assume A24: Hom (d1,c4) <> {} ; :: thesis: ( not f4 * g1 = f6 * g2 or ( 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 ) ) ) )

assume A25: f4 * g1 = f6 * g2 ; :: thesis: ( 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 ) ) )

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: 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 ) )

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: ( f1 * h = g1 & f3 * h = g2 & ( for h1 being Morphism of d1,c1 st f1 * h1 = g1 & f3 * h1 = g2 holds

h = h1 ) )

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: ( f3 * h = g2 & ( for h1 being Morphism of d1,c1 st f1 * h1 = g1 & f3 * h1 = g2 holds

h = h1 ) )

thus f3 * h = g2 by A30; :: thesis: for h1 being Morphism of d1,c1 st f1 * h1 = g1 & f3 * h1 = g2 holds

h = h1

let h1 be Morphism of d1,c1; :: thesis: ( f1 * h1 = g1 & f3 * h1 = g2 implies h = h1 )

assume A36: f1 * h1 = g1 ; :: thesis: ( not f3 * h1 = g2 or h = h1 )

A37: (f2 * f1) * h1 = f2 * g1 by A1, A36, A29, Th23;

assume f3 * h1 = g2 ; :: thesis: h = h1

hence h = h1 by A30, A37; :: thesis: verum