let M1, M2 be Function of L,(InclPoset (Ids L)); :: thesis: ( ( for x being Element of L holds
( ( x <= sup I implies M1 . x = (downarrow x) /\ I ) & ( not x <= sup I implies M1 . x = downarrow x ) ) ) & ( for x being Element of L holds
( ( x <= sup I implies M2 . x = (downarrow x) /\ I ) & ( not x <= sup I implies M2 . x = downarrow x ) ) ) implies M1 = M2 )
assume A4: for x being Element of L holds
( ( x <= sup I implies M1 . x = (downarrow x) /\ I ) & ( not x <= sup I implies M1 . x = downarrow x ) ) ; :: thesis: ( ex x being Element of L st
( ( x <= sup I implies M2 . x = (downarrow x) /\ I ) implies ( not x <= sup I & not M2 . x = downarrow x ) ) or M1 = M2 )
assume A5: for x being Element of L holds
( ( x <= sup I implies M2 . x = (downarrow x) /\ I ) & ( not x <= sup I implies M2 . x = downarrow x ) ) ; :: thesis: M1 = M2
A6: dom M1 = the carrier of L by FUNCT_2:def 1;
A7: dom M2 = the carrier of L by FUNCT_2:def 1;
now :: thesis: for x being object st x in the carrier of L holds
M1 . x = M2 . x
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 ;
A8: now :: thesis: ( x9 <= sup I implies M1 . x9 = M2 . x9 )
assume A9: x9 <= sup I ; :: thesis: M1 . x9 = M2 . x9
then M1 . x9 = (downarrow x9) /\ I by A4;
hence M1 . x9 = M2 . x9 by A5, A9; :: thesis: verum
end;
now :: thesis: ( not x9 <= sup I implies M1 . x9 = M2 . x9 )
assume A10: not x9 <= sup I ; :: thesis: M1 . x9 = M2 . x9
then M1 . x9 = downarrow x9 by A4;
hence M1 . x9 = M2 . x9 by A5, A10; :: thesis: verum
end;
hence M1 . x = M2 . x by A8; :: thesis: verum
end;
hence M1 = M2 by A6, A7, FUNCT_1:2; :: thesis: verum