A3:
( a [x] c, pr1 (a,c), pr2 (a,c) is_product_of a,c & Hom ((a [x] c),a) <> {} & Hom ((a [x] c),c) <> {} )
by Th42;
A4:
( b [x] d, pr1 (b,d), pr2 (b,d) is_product_of b,d & Hom ((b [x] d),b) <> {} & Hom ((b [x] d),d) <> {} )
by Th42;
( Hom ((a [x] c),b) <> {} & Hom ((a [x] c),d) <> {} )
by A3, A1, A2, CAT_7:22;
then consider h being Morphism of a [x] c,b [x] d such that
A5:
( (pr1 (b,d)) * h = f * (pr1 (a,c)) & (pr2 (b,d)) * h = g * (pr2 (a,c)) & ( for h1 being Morphism of a [x] c,b [x] d st (pr1 (b,d)) * h1 = f * (pr1 (a,c)) & (pr2 (b,d)) * h1 = g * (pr2 (a,c)) holds
h = h1 ) )
by A4, Def10;
for h1, h2 being Morphism of a [x] c,b [x] d st f * (pr1 (a,c)) = (pr1 (b,d)) * h1 & g * (pr2 (a,c)) = (pr2 (b,d)) * h1 & f * (pr1 (a,c)) = (pr1 (b,d)) * h2 & g * (pr2 (a,c)) = (pr2 (b,d)) * h2 holds
h1 = h2
proof
let h1,
h2 be
Morphism of
a [x] c,
b [x] d;
( f * (pr1 (a,c)) = (pr1 (b,d)) * h1 & g * (pr2 (a,c)) = (pr2 (b,d)) * h1 & f * (pr1 (a,c)) = (pr1 (b,d)) * h2 & g * (pr2 (a,c)) = (pr2 (b,d)) * h2 implies h1 = h2 )
assume A6:
(
f * (pr1 (a,c)) = (pr1 (b,d)) * h1 &
g * (pr2 (a,c)) = (pr2 (b,d)) * h1 )
;
( not f * (pr1 (a,c)) = (pr1 (b,d)) * h2 or not g * (pr2 (a,c)) = (pr2 (b,d)) * h2 or h1 = h2 )
assume A7:
(
f * (pr1 (a,c)) = (pr1 (b,d)) * h2 &
g * (pr2 (a,c)) = (pr2 (b,d)) * h2 )
;
h1 = h2
thus h1 =
h
by A6, A5
.=
h2
by A5, A7
;
verum
end;
hence
( ex b1 being Morphism of a [x] c,b [x] d st
( f * (pr1 (a,c)) = (pr1 (b,d)) * b1 & g * (pr2 (a,c)) = (pr2 (b,d)) * b1 ) & ( for b1, b2 being Morphism of a [x] c,b [x] d st f * (pr1 (a,c)) = (pr1 (b,d)) * b1 & g * (pr2 (a,c)) = (pr2 (b,d)) * b1 & f * (pr1 (a,c)) = (pr1 (b,d)) * b2 & g * (pr2 (a,c)) = (pr2 (b,d)) * b2 holds
b1 = b2 ) )
by A5; verum