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 S₁[ 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 & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in (Concretized A) -carrier_of a implies ex y being object st
( y in (Concretized A) -carrier_of b & S₁[x,y] ) )
assume x in (Concretized A) -carrier_of a ; :: thesis: ex y being object st
( y in (Concretized A) -carrier_of b & S₁[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]] ; :: thesis: ( [(f * g),[o,b]] in (Concretized A) -carrier_of b & S₁[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 & S₁[x,[(f * g),[o,b]]] ) by A3, A4, Th43; :: thesis: 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
S₁[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 ; :: 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 A8: <^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 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; :: thesis: verum

end;

hence F in the Arrows of (Concretized A) . (a,b) by A7, 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 <^c,a^> <> {} ; :: thesis: 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; :: thesis: verum