let A be category; :: thesis: for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b ex F being Function of ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b) st
( F in the Arrows of (Concretized A) . a,b & ( for c being object of A
for g being Morphism of c,a st <^c,a^> <> {} holds
F . [g,[c,a]] = [(f * g),[c,b]] ) )
let a, b be object of A; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex F being Function of ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b) st
( F in the Arrows of (Concretized A) . a,b & ( for c being object of A
for g being Morphism of c,a st <^c,a^> <> {} holds
F . [g,[c,a]] = [(f * g),[c,b]] ) ) )
assume A1:
<^a,b^> <> {}
; :: thesis: for f being Morphism of a,b ex F being Function of ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b) st
( F in the Arrows of (Concretized A) . a,b & ( for c being object of A
for g being Morphism of c,a st <^c,a^> <> {} holds
F . [g,[c,a]] = [(f * g),[c,b]] ) )
set B = Concretized A;
let f be Morphism of a,b; :: thesis: ex F being Function of ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b) st
( F in the Arrows of (Concretized A) . a,b & ( for c being object of A
for g being Morphism of c,a st <^c,a^> <> {} holds
F . [g,[c,a]] = [(f * g),[c,b]] ) )
defpred S1[ set , set ] means ex o being object of A ex g being Morphism of o,a st
( <^o,a^> <> {} & $1 = [g,[o,a]] & $2 = [(f * g),[o,b]] );
A2:
for x being set st x in (Concretized A) -carrier_of a holds
ex y being set st
( y in (Concretized A) -carrier_of b & S1[x,y] )
proof
let x be
set ;
:: thesis: ( x in (Concretized A) -carrier_of a implies ex y being set st
( y in (Concretized A) -carrier_of b & S1[x,y] ) )
assume
x in (Concretized A) -carrier_of a
;
:: thesis: ex y being set st
( y in (Concretized A) -carrier_of b & S1[x,y] )
then consider o being
object of
A,
g being
Morphism of
o,
a such that A3:
(
<^o,a^> <> {} &
x = [g,[o,a]] )
by Th45;
take
[(f * g),[o,b]]
;
:: thesis: ( [(f * g),[o,b]] in (Concretized A) -carrier_of b & S1[x,[(f * g),[o,b]]] )
<^o,b^> <> {}
by A1, A3, ALTCAT_1:def 4;
hence
(
[(f * g),[o,b]] in (Concretized A) -carrier_of b &
S1[
x,
[(f * g),[o,b]]] )
by A3, Th45;
:: thesis: verum
end;
consider F being Function such that
A4:
( dom F = (Concretized A) -carrier_of a & rng F c= (Concretized A) -carrier_of b )
and
A5:
for x being set st x in (Concretized A) -carrier_of a holds
S1[x,F . x]
from WELLORD2:sch 1(A2);
A6:
F in Funcs ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b)
by A4, FUNCT_2:def 2;
then reconsider F = F as Function of ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b) by FUNCT_2:121;
take
F
; :: thesis: ( F in the Arrows of (Concretized A) . a,b & ( for c being object of A
for g being Morphism of c,a st <^c,a^> <> {} holds
F . [g,[c,a]] = [(f * g),[c,b]] ) )
ex fa, fb being object of A ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of A st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds F . [h,[o,fa]] = [(g * h),[o,fb]] ) )
proof
take fa =
a;
:: thesis: ex fb being object of A ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of A st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds F . [h,[o,fa]] = [(g * h),[o,fb]] ) )
take fb =
b;
:: thesis: ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of A st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds F . [h,[o,fa]] = [(g * h),[o,fb]] ) )
reconsider g =
f as
Morphism of
fa,
fb ;
take
g
;
:: thesis: ( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being object of A st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds F . [h,[o,fa]] = [(g * h),[o,fb]] ) )
thus
(
fa = a &
fb = b &
<^fa,fb^> <> {} )
by A1;
:: thesis: for o being object of A st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds F . [h,[o,fa]] = [(g * h),[o,fb]]
let o be
object of
A;
:: thesis: ( <^o,fa^> <> {} implies for h being Morphism of o,fa holds F . [h,[o,fa]] = [(g * h),[o,fb]] )
assume A7:
<^o,fa^> <> {}
;
:: thesis: for h being Morphism of o,fa holds F . [h,[o,fa]] = [(g * h),[o,fb]]
let h be
Morphism of
o,
fa;
:: thesis: F . [h,[o,fa]] = [(g * h),[o,fb]]
[h,[o,fa]] in (Concretized A) -carrier_of fa
by A7, Th45;
then consider c being
object of
A,
k being
Morphism of
c,
fa such that A8:
(
<^c,fa^> <> {} &
[h,[o,fa]] = [k,[c,fa]] &
F . [h,[o,fa]] = [(g * k),[c,fb]] )
by A5;
[o,fa] = [c,fa]
by A8, ZFMISC_1:33;
then
(
o = c &
h = k )
by A8, ZFMISC_1:33;
hence
F . [h,[o,fa]] = [(g * h),[o,fb]]
by A8;
:: thesis: verum
end;
hence
F in the Arrows of (Concretized A) . a,b
by A6, Def12; :: thesis: for c being object of A
for g being Morphism of c,a st <^c,a^> <> {} holds
F . [g,[c,a]] = [(f * g),[c,b]]
let c be object of A; :: thesis: for g being Morphism of c,a st <^c,a^> <> {} holds
F . [g,[c,a]] = [(f * g),[c,b]]
let g be Morphism of c,a; :: thesis: ( <^c,a^> <> {} implies F . [g,[c,a]] = [(f * g),[c,b]] )
assume A9:
<^c,a^> <> {}
; :: thesis: F . [g,[c,a]] = [(f * g),[c,b]]
[g,[c,a]] in (Concretized A) -carrier_of a
by A9, Th45;
then consider o being object of A, h being Morphism of o,a such that
A10:
( <^o,a^> <> {} & [g,[c,a]] = [h,[o,a]] & F . [g,[c,a]] = [(f * h),[o,b]] )
by A5;
[c,a] = [o,a]
by A10, ZFMISC_1:33;
then
( c = o & g = h )
by A10, ZFMISC_1:33;
hence
F . [g,[c,a]] = [(f * g),[c,b]]
by A10; :: thesis: verum