let f, g be PartFunc of F_{1}(),F_{2}(); :: thesis: ( dom f = F_{3}() & ( for c being Element of F_{1}() st c in dom f holds

f . c = F_{4}(c) ) & dom g = F_{3}() & ( for c being Element of F_{1}() st c in dom g holds

g . c = F_{4}(c) ) implies f = g )

assume that

A1: dom f = F_{3}()
and

A2: for c being Element of F_{1}() st c in dom f holds

f . c = F_{4}(c)
and

A3: dom g = F_{3}()
and

A4: for c being Element of F_{1}() st c in dom g holds

g . c = F_{4}(c)
; :: thesis: f = g

f . c = F

g . c = F

assume that

A1: dom f = F

A2: for c being Element of F

f . c = F

A3: dom g = F

A4: for c being Element of F

g . c = F

now :: thesis: for c being Element of F_{1}() st c in dom f holds

f . c = g . c

hence
f = g
by A1, A3, PARTFUN1:5; :: thesis: verumf . c = g . c

let c be Element of F_{1}(); :: thesis: ( c in dom f implies f . c = g . c )

assume A5: c in dom f ; :: thesis: f . c = g . c

hence f . c = F_{4}(c)
by A2

.= g . c by A1, A3, A4, A5 ;

:: thesis: verum

end;assume A5: c in dom f ; :: thesis: f . c = g . c

hence f . c = F

.= g . c by A1, A3, A4, A5 ;

:: thesis: verum