let f, g be PartFunc of F1(),F2(); :: thesis: ( dom f = F3() & ( for c being Element of F1() st c indom f holds f . c = F4(c) ) & dom g = F3() & ( for c being Element of F1() st c indom g holds g . c = F4(c) ) implies f = g ) assume that A1:
dom f = F3()
and A2:
for c being Element of F1() st c indom f holds f . c = F4(c)
and A3:
dom g = F3()
and A4:
for c being Element of F1() st c indom g holds g . c = F4(c)
; :: thesis: f = g