let h, g be Function; :: thesis: ( dom h = (dom f) \ (f " {0}) & ( for c being object st c in dom h holds

h . c = (f . c) " ) & dom g = (dom f) \ (f " {0}) & ( for c being object st c in dom g holds

g . c = (f . c) " ) implies h = g )

assume that

A1: dom h = (dom f) \ (f " {0}) and

A2: for c being object st c in dom h holds

h . c = (f . c) " and

A3: dom g = (dom f) \ (f " {0}) and

A4: for c being object st c in dom g holds

g . c = (f . c) " ; :: thesis: h = g

h . c = (f . c) " ) & dom g = (dom f) \ (f " {0}) & ( for c being object st c in dom g holds

g . c = (f . c) " ) implies h = g )

assume that

A1: dom h = (dom f) \ (f " {0}) and

A2: for c being object st c in dom h holds

h . c = (f . c) " and

A3: dom g = (dom f) \ (f " {0}) and

A4: for c being object st c in dom g holds

g . c = (f . c) " ; :: thesis: h = g

now :: thesis: for x being object st x in dom h holds

h . x = g . x

hence
h = g
by A1, A3, FUNCT_1:2; :: thesis: verumh . x = g . x

let x be object ; :: thesis: ( x in dom h implies h . x = g . x )

assume A5: x in dom h ; :: thesis: h . x = g . x

hence h . x = (f . x) " by A2

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

:: thesis: verum

end;assume A5: x in dom h ; :: thesis: h . x = g . x

hence h . x = (f . x) " by A2

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

:: thesis: verum