set IT = X --> L;
let x be set ; :: according to PRALG_1:def 11 :: thesis: ( not x in dom (X --> L) or (X --> L) . x is 1-sorted )
assume A1: x in dom (X --> L) ; :: thesis: (X --> L) . x is 1-sorted
then x in X by PBOOLE:def 3;
then A2: rng (X --> L) = {L} by FUNCOP_1:14;
(X --> L) . x in rng (X --> L) by A1, FUNCT_1:def 5;
hence (X --> L) . x is 1-sorted by A2, TARSKI:def 1; :: thesis: verum