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, Th1; :: 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