let F1, F2 be Function; :: thesis: ( dom F1 = dom f & ( for x being object st x in dom F1 holds

F1 . x = |[(f . x)]| ) & dom F2 = dom f & ( for x being object st x in dom F2 holds

F2 . x = |[(f . x)]| ) implies F1 = F2 )

assume that

A1: dom F1 = dom f and

A2: for x being object st x in dom F1 holds

F1 . x = |[(f . x)]| and

A3: dom F2 = dom f and

A4: for x being object st x in dom F2 holds

F2 . x = |[(f . x)]| ; :: thesis: F1 = F2

F1 . x = |[(f . x)]| ) & dom F2 = dom f & ( for x being object st x in dom F2 holds

F2 . x = |[(f . x)]| ) implies F1 = F2 )

assume that

A1: dom F1 = dom f and

A2: for x being object st x in dom F1 holds

F1 . x = |[(f . x)]| and

A3: dom F2 = dom f and

A4: for x being object st x in dom F2 holds

F2 . x = |[(f . x)]| ; :: thesis: F1 = F2

now :: thesis: for x being set st x in dom F1 holds

F1 . x = F2 . x

hence
F1 = F2
by A1, A3; :: thesis: verumF1 . x = F2 . x

let x be set ; :: thesis: ( x in dom F1 implies F1 . x = F2 . x )

assume A5: x in dom F1 ; :: thesis: F1 . x = F2 . x

hence F1 . x = |[(f . x)]| by A2

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

:: thesis: verum

end;assume A5: x in dom F1 ; :: thesis: F1 . x = F2 . x

hence F1 . x = |[(f . x)]| by A2

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

:: thesis: verum