let C be category; :: thesis: for c, c1, c2, d being Object of C

for f1 being Morphism of c1,c

for f2 being Morphism of c2,c

for p1 being Morphism of d,c1

for p2 being Morphism of d,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 holds

d,p2,p1 is_pullback_of f2,f1

let c, c1, c2, d be Object of C; :: thesis: for f1 being Morphism of c1,c

for f2 being Morphism of c2,c

for p1 being Morphism of d,c1

for p2 being Morphism of d,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 holds

d,p2,p1 is_pullback_of f2,f1

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

for p1 being Morphism of d,c1

for p2 being Morphism of d,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 holds

d,p2,p1 is_pullback_of f2,f1

let f2 be Morphism of c2,c; :: thesis: for p1 being Morphism of d,c1

for p2 being Morphism of d,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 holds

d,p2,p1 is_pullback_of f2,f1

let p1 be Morphism of d,c1; :: thesis: for p2 being Morphism of d,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 holds

d,p2,p1 is_pullback_of f2,f1

let p2 be Morphism of d,c2; :: thesis: ( Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 implies d,p2,p1 is_pullback_of f2,f1 )

assume A1: ( Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} ) ; :: thesis: ( not d,p1,p2 is_pullback_of f1,f2 or d,p2,p1 is_pullback_of f2,f1 )

assume A2: d,p1,p2 is_pullback_of f1,f2 ; :: thesis: d,p2,p1 is_pullback_of f2,f1

then A3: ( f1 * p1 = f2 * p2 & ( for d1 being Object of C

for g1 being Morphism of d1,c1

for g2 being Morphism of d1,c2 st Hom (d1,c1) <> {} & Hom (d1,c2) <> {} & f1 * g1 = f2 * g2 holds

( Hom (d1,d) <> {} & ex h being Morphism of d1,d st

( p1 * h = g1 & p2 * h = g2 & ( for h1 being Morphism of d1,d st p1 * h1 = g1 & p2 * h1 = g2 holds

h = h1 ) ) ) ) ) by A1, Def17;

for d1 being Object of C

for g2 being Morphism of d1,c2

for g1 being Morphism of d1,c1 st Hom (d1,c2) <> {} & Hom (d1,c1) <> {} & f2 * g2 = f1 * g1 holds

( Hom (d1,d) <> {} & ex h being Morphism of d1,d st

( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) ) )

for f1 being Morphism of c1,c

for f2 being Morphism of c2,c

for p1 being Morphism of d,c1

for p2 being Morphism of d,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 holds

d,p2,p1 is_pullback_of f2,f1

let c, c1, c2, d be Object of C; :: thesis: for f1 being Morphism of c1,c

for f2 being Morphism of c2,c

for p1 being Morphism of d,c1

for p2 being Morphism of d,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 holds

d,p2,p1 is_pullback_of f2,f1

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

for p1 being Morphism of d,c1

for p2 being Morphism of d,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 holds

d,p2,p1 is_pullback_of f2,f1

let f2 be Morphism of c2,c; :: thesis: for p1 being Morphism of d,c1

for p2 being Morphism of d,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 holds

d,p2,p1 is_pullback_of f2,f1

let p1 be Morphism of d,c1; :: thesis: for p2 being Morphism of d,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 holds

d,p2,p1 is_pullback_of f2,f1

let p2 be Morphism of d,c2; :: thesis: ( Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 implies d,p2,p1 is_pullback_of f2,f1 )

assume A1: ( Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} ) ; :: thesis: ( not d,p1,p2 is_pullback_of f1,f2 or d,p2,p1 is_pullback_of f2,f1 )

assume A2: d,p1,p2 is_pullback_of f1,f2 ; :: thesis: d,p2,p1 is_pullback_of f2,f1

then A3: ( f1 * p1 = f2 * p2 & ( for d1 being Object of C

for g1 being Morphism of d1,c1

for g2 being Morphism of d1,c2 st Hom (d1,c1) <> {} & Hom (d1,c2) <> {} & f1 * g1 = f2 * g2 holds

( Hom (d1,d) <> {} & ex h being Morphism of d1,d st

( p1 * h = g1 & p2 * h = g2 & ( for h1 being Morphism of d1,d st p1 * h1 = g1 & p2 * h1 = g2 holds

h = h1 ) ) ) ) ) by A1, Def17;

for d1 being Object of C

for g2 being Morphism of d1,c2

for g1 being Morphism of d1,c1 st Hom (d1,c2) <> {} & Hom (d1,c1) <> {} & f2 * g2 = f1 * g1 holds

( Hom (d1,d) <> {} & ex h being Morphism of d1,d st

( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) ) )

proof

hence
d,p2,p1 is_pullback_of f2,f1
by A3, A1, Def17; :: thesis: verum
let d1 be Object of C; :: thesis: for g2 being Morphism of d1,c2

for g1 being Morphism of d1,c1 st Hom (d1,c2) <> {} & Hom (d1,c1) <> {} & f2 * g2 = f1 * g1 holds

( Hom (d1,d) <> {} & ex h being Morphism of d1,d st

( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) ) )

let g2 be Morphism of d1,c2; :: thesis: for g1 being Morphism of d1,c1 st Hom (d1,c2) <> {} & Hom (d1,c1) <> {} & f2 * g2 = f1 * g1 holds

( Hom (d1,d) <> {} & ex h being Morphism of d1,d st

( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) ) )

let g1 be Morphism of d1,c1; :: thesis: ( Hom (d1,c2) <> {} & Hom (d1,c1) <> {} & f2 * g2 = f1 * g1 implies ( Hom (d1,d) <> {} & ex h being Morphism of d1,d st

( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) ) ) )

assume A4: ( Hom (d1,c2) <> {} & Hom (d1,c1) <> {} & f2 * g2 = f1 * g1 ) ; :: thesis: ( Hom (d1,d) <> {} & ex h being Morphism of d1,d st

( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) ) )

hence Hom (d1,d) <> {} by A2, A1, Def17; :: thesis: ex h being Morphism of d1,d st

( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) )

consider h being Morphism of d1,d such that

A5: ( p1 * h = g1 & p2 * h = g2 & ( for h1 being Morphism of d1,d st p1 * h1 = g1 & p2 * h1 = g2 holds

h = h1 ) ) by A4, A2, A1, Def17;

take h ; :: thesis: ( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) )

thus ( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) ) by A5; :: thesis: verum

end;for g1 being Morphism of d1,c1 st Hom (d1,c2) <> {} & Hom (d1,c1) <> {} & f2 * g2 = f1 * g1 holds

( Hom (d1,d) <> {} & ex h being Morphism of d1,d st

( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) ) )

let g2 be Morphism of d1,c2; :: thesis: for g1 being Morphism of d1,c1 st Hom (d1,c2) <> {} & Hom (d1,c1) <> {} & f2 * g2 = f1 * g1 holds

( Hom (d1,d) <> {} & ex h being Morphism of d1,d st

( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) ) )

let g1 be Morphism of d1,c1; :: thesis: ( Hom (d1,c2) <> {} & Hom (d1,c1) <> {} & f2 * g2 = f1 * g1 implies ( Hom (d1,d) <> {} & ex h being Morphism of d1,d st

( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) ) ) )

assume A4: ( Hom (d1,c2) <> {} & Hom (d1,c1) <> {} & f2 * g2 = f1 * g1 ) ; :: thesis: ( Hom (d1,d) <> {} & ex h being Morphism of d1,d st

( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) ) )

hence Hom (d1,d) <> {} by A2, A1, Def17; :: thesis: ex h being Morphism of d1,d st

( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) )

consider h being Morphism of d1,d such that

A5: ( p1 * h = g1 & p2 * h = g2 & ( for h1 being Morphism of d1,d st p1 * h1 = g1 & p2 * h1 = g2 holds

h = h1 ) ) by A4, A2, A1, Def17;

take h ; :: thesis: ( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) )

thus ( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds

h = h1 ) ) by A5; :: thesis: verum