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
proof
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;
hence M1 = M2 by FUNCT_2:12; :: thesis: verum