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₁[ 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 & S₁[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 & S₁[x,y] ) )
assume x in (Concretized A) -carrier_of a ; :: thesis: ex y being set 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 Th45;
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 4;
hence ( [(f * g),[o,b]] in (Concretized A) -carrier_of b & S₁[x,[(f * g),[o,b]]] ) by A3, A4, Th45; :: 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 set st x in (Concretized A) -carrier_of a holds
S₁[x,F . x] from WELLORD2:sch 1(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: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 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, Th45;
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, ZFMISC_1:33;
then o = c by ZFMISC_1:33;
hence F . [h,[o,fa]] = [(g * h),[o,fb]] by A9, A10, ZFMISC_1:33; :: 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 Th45;
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, ZFMISC_1:33;
then c = o by ZFMISC_1:33;
hence F . [g,[c,a]] = [(f * g),[c,b]] by A11, A12, ZFMISC_1:33; :: thesis: verum