let f1, f2 be PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)); :: thesis: ( dom f1 = { [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 f1 holds
f1 . [k,k9] = k * k9 ) & dom f2 = { [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 f2 holds
f2 . [k,k9] = k * k9 ) implies f1 = f2 )
assume that
A9: ( dom f1 = { [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 f1 holds
f1 . [k,k9] = k * k9 ) ) and
A10: ( dom f2 = { [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 f2 holds
f2 . [k,k9] = k * k9 ) ) ; :: thesis: f1 = f2

now :: thesis: for x being object st x in { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } implies f1 . x = f2 . x )
assume A11: x in { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } ; :: thesis: f1 . x = f2 . x
then consider k1, k2 being Element of commaMorphs (F,G) such that
A12: x = [k1,k2] and
k1 `11 = k2 `12 ;
thus f1 . x = k1 * k2 by A9, A11, A12
.= f2 . x by A10, A11, A12 ; :: thesis: verum

end;

hence f1 = f2 by A9, A10, FUNCT_1:2; :: thesis: verum