let A be category; 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; ( <^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^> <> {}
; 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; 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[ object , object ] 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 object st x in (Concretized A) -carrier_of a holds
ex y being object st
( y in (Concretized A) -carrier_of b & S1[x,y] )
proof
let x be
object ;
( x in (Concretized A) -carrier_of a implies ex y being object st
( y in (Concretized A) -carrier_of b & S1[x,y] ) )
assume
x in (Concretized A) -carrier_of a
;
ex y being object 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^> <> {}
and A4:
x = [g,[o,a]]
by Th43;
take
[(f * g),[o,b]]
;
( [(f * g),[o,b]] in (Concretized A) -carrier_of b & S1[x,[(f * g),[o,b]]] )
<^o,b^> <> {}
by A1, A3, ALTCAT_1:def 2;
hence
(
[(f * g),[o,b]] in (Concretized A) -carrier_of b &
S1[
x,
[(f * g),[o,b]]] )
by A3, A4, Th43;
verum
end;
consider F being Function such that
A5:
( dom F = (Concretized A) -carrier_of a & rng F c= (Concretized A) -carrier_of b )
and
A6:
for x being object st x in (Concretized A) -carrier_of a holds
S1[x,F . x]
from FUNCT_1:sch 6(A2);
A7:
F in Funcs (((Concretized A) -carrier_of a),((Concretized A) -carrier_of b))
by A5, FUNCT_2:def 2;
then reconsider F = F as Function of ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b) by FUNCT_2:66;
take
F
; ( 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;
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;
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
;
( 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;
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;
( <^o,fa^> <> {} implies for h being Morphism of o,fa holds F . [h,[o,fa]] = [(g * h),[o,fb]] )
assume A8:
<^o,fa^> <> {}
;
for h being Morphism of o,fa holds F . [h,[o,fa]] = [(g * h),[o,fb]]
let h be
Morphism of
o,
fa;
F . [h,[o,fa]] = [(g * h),[o,fb]]
[h,[o,fa]] in (Concretized A) -carrier_of fa
by A8, Th43;
then consider c being
Object of
A,
k being
Morphism of
c,
fa such that
<^c,fa^> <> {}
and A9:
[h,[o,fa]] = [k,[c,fa]]
and A10:
F . [h,[o,fa]] = [(g * k),[c,fb]]
by A6;
[o,fa] = [c,fa]
by A9, XTUPLE_0:1;
then
o = c
by XTUPLE_0:1;
hence
F . [h,[o,fa]] = [(g * h),[o,fb]]
by A9, A10, XTUPLE_0:1;
verum
end;
hence
F in the Arrows of (Concretized A) . (a,b)
by A7, Def12; 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; 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; ( <^c,a^> <> {} implies F . [g,[c,a]] = [(f * g),[c,b]] )
assume
<^c,a^> <> {}
; F . [g,[c,a]] = [(f * g),[c,b]]
then
[g,[c,a]] in (Concretized A) -carrier_of a
by Th43;
then consider o being Object of A, h being Morphism of o,a such that
<^o,a^> <> {}
and
A11:
[g,[c,a]] = [h,[o,a]]
and
A12:
F . [g,[c,a]] = [(f * h),[o,b]]
by A6;
[c,a] = [o,a]
by A11, XTUPLE_0:1;
then
c = o
by XTUPLE_0:1;
hence
F . [g,[c,a]] = [(f * g),[c,b]]
by A11, A12, XTUPLE_0:1; verum