let fa, fb be Function; :: thesis: ( dom fa = dom f & ( for i being object st i in dom f holds
fa . i = (f . i) mod m ) & dom fb = dom f & ( for i being object st i in dom f holds
fb . i = (f . i) mod m ) implies fa = fb )
assume that
A5: dom f = dom fa and
A6: for i being object st i in dom f holds
fa . i = (f . i) mod m and
A7: dom f = dom fb and
A8: for i being object st i in dom f holds
fb . i = (f . i) mod m ; :: thesis: fa = fb

now :: thesis: for X being set st dom f = X holds
fa = fb

let X be set ; :: thesis: ( dom f = X implies fa = fb )
assume A9: dom f = X ; :: thesis: fa = fb
for i being object st i in X holds
fa . i = fb . i

proof

given j being object such that A11: j in X and
A12: fa . j <> fb . j ; :: thesis: contradiction
fa . j <> (f . j) mod m by A8, A9, A11, A12;
hence contradiction by A6, A9, A11; :: thesis: verum

end;

hence fa = fb by A5, A7, A9; :: thesis: verum

end;

hence fa = fb ; :: thesis: verum