let M1, M2 be Function of L,(InclPoset (LOWER L)); :: thesis: ( ( for x being Element of L holds M1 . x = R -below x ) & ( for x being Element of L holds M2 . x = R -below x ) implies M1 = M2 )

assume A3: for x being Element of L holds M1 . x = R -below x ; :: thesis: ( ex x being Element of L st not M2 . x = R -below x or M1 = M2 )

assume A4: for x being Element of L holds M2 . x = R -below x ; :: thesis: M1 = M2

for x being object st x in the carrier of L holds

M1 . x = M2 . x

assume A3: for x being Element of L holds M1 . x = R -below x ; :: thesis: ( ex x being Element of L st not M2 . x = R -below x or M1 = M2 )

assume A4: for x being Element of L holds M2 . x = R -below x ; :: thesis: M1 = M2

for x being object st x in the carrier of L holds

M1 . x = M2 . x

proof

hence
M1 = M2
by FUNCT_2:12; :: thesis: verum
let x be object ; :: thesis: ( x in the carrier of L implies M1 . x = M2 . x )

assume x in the carrier of L ; :: thesis: M1 . x = M2 . x

then reconsider x9 = x as Element of L ;

thus M1 . x = R -below x9 by A3

.= M2 . x by A4 ; :: thesis: verum

end;assume x in the carrier of L ; :: thesis: M1 . x = M2 . x

then reconsider x9 = x as Element of L ;

thus M1 . x = R -below x9 by A3

.= M2 . x by A4 ; :: thesis: verum