let M1, M2 be Function of X,REAL; :: thesis: ( ( for x being set st x in X holds

M1 . x = min (r,(f . x)) ) & ( for x being set st x in X holds

M2 . x = min (r,(f . x)) ) implies M1 = M2 )

assume that

A3: for x being set st x in X holds

M1 . x = min (r,(f . x)) and

A4: for x being set st x in X holds

M2 . x = min (r,(f . x)) ; :: thesis: M1 = M2

M1 . x = min (r,(f . x)) ) & ( for x being set st x in X holds

M2 . x = min (r,(f . x)) ) implies M1 = M2 )

assume that

A3: for x being set st x in X holds

M1 . x = min (r,(f . x)) and

A4: for x being set st x in X holds

M2 . x = min (r,(f . x)) ; :: thesis: M1 = M2

now :: thesis: for x being object st x in X holds

M1 . x = M2 . x

hence
M1 = M2
by FUNCT_2:12; :: thesis: verumM1 . x = M2 . x

let x be object ; :: thesis: ( x in X implies M1 . x = M2 . x )

assume A5: x in X ; :: thesis: M1 . x = M2 . x

reconsider y = x as Element of X by A5;

M1 . x = H_{1}(y)
by A3, A5;

hence M1 . x = M2 . x by A4, A5; :: thesis: verum

end;assume A5: x in X ; :: thesis: M1 . x = M2 . x

reconsider y = x as Element of X by A5;

M1 . x = H

hence M1 . x = M2 . x by A4, A5; :: thesis: verum