let f1, f2 be PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)); ( 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 ) )
; f1 = f2
now 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 . xlet x be
object ;
( 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 }
;
f1 . x = f2 . xthen 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
;
verum end;
hence
f1 = f2
by A9, A10, FUNCT_1:2; verum