defpred S₁[ set , set ] means ex k1, k2 being Element of commaMorphs F,G st
( $1 = [k1,k2] & $2 = k1 * k2 );
set X = { [k1,k2] where k1, k2 is Element of commaMorphs F,G : k1 `11 = k2 `12 } ;
A1: for x being set st x in { [k1,k2] where k1, k2 is Element of commaMorphs F,G : k1 `11 = k2 `12 } holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in { [k1,k2] where k1, k2 is Element of commaMorphs F,G : k1 `11 = k2 `12 } implies ex y being set st S₁[x,y] )
assume x in { [k1,k2] where k1, k2 is Element of commaMorphs F,G : k1 `11 = k2 `12 } ; :: thesis: ex y being set st S₁[x,y]
then consider k1, k2 being Element of commaMorphs F,G such that
A2: x = [k1,k2] and
k1 `11 = k2 `12 ;
reconsider y = k1 * k2 as set ;
take y ; :: thesis: S₁[x,y]
take k1 ; :: thesis: ex k2 being Element of commaMorphs F,G st
( x = [k1,k2] & y = k1 * k2 )
take k2 ; :: thesis: ( x = [k1,k2] & y = k1 * k2 )
thus ( x = [k1,k2] & y = k1 * k2 ) by A2; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = { [k1,k2] where k1, k2 is Element of commaMorphs F,G : k1 `11 = k2 `12 } & ( for x being set st x in { [k1,k2] where k1, k2 is Element of commaMorphs F,G : k1 `11 = k2 `12 } holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A1);
A4: rng f c= commaMorphs F,G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in commaMorphs F,G )
assume x in rng f ; :: thesis: x in commaMorphs F,G
then consider y being set such that
A5: y in dom f and
A6: x = f . y by FUNCT_1:def 5;
ex k1, k2 being Element of commaMorphs F,G st
( y = [k1,k2] & f . y = k1 * k2 ) by A3, A5;
hence x in commaMorphs F,G by A6; :: thesis: verum

end;

dom f c= [:(commaMorphs F,G),(commaMorphs F,G):]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in [:(commaMorphs F,G),(commaMorphs F,G):] )
assume x in dom f ; :: thesis: x in [:(commaMorphs F,G),(commaMorphs F,G):]
then ex k1, k2 being Element of commaMorphs F,G st
( x = [k1,k2] & k1 `11 = k2 `12 ) by A3;
hence x in [:(commaMorphs F,G),(commaMorphs F,G):] ; :: thesis: verum

end;

then reconsider f = f as PartFunc of [:(commaMorphs F,G),(commaMorphs F,G):],(commaMorphs F,G) by A4, RELSET_1:11;
take f ; :: thesis: ( dom f = { [k1,k2] where k1, k2 is Element of commaMorphs F,G : k1 `11 = k2 `12 } & ( for k, k9 being Element of commaMorphs F,G st [k,k9] in dom f holds
f . [k,k9] = k * k9 ) )
thus dom f = { [k1,k2] where k1, k2 is Element of commaMorphs F,G : k1 `11 = k2 `12 } by A3; :: thesis: for k, k9 being Element of commaMorphs F,G st [k,k9] in dom f holds
f . [k,k9] = k * k9
let k1, k2 be Element of commaMorphs F,G; :: thesis: ( [k1,k2] in dom f implies f . [k1,k2] = k1 * k2 )
assume [k1,k2] in dom f ; :: thesis: f . [k1,k2] = k1 * k2
then consider k, k9 being Element of commaMorphs F,G such that
A7: [k1,k2] = [k,k9] and
A8: f . [k1,k2] = k * k9 by A3;
k1 = k by A7, ZFMISC_1:33;
hence f . [k1,k2] = k1 * k2 by A7, A8, ZFMISC_1:33; :: thesis: verum