let x be object ; :: according to PRALG_1:def 12 :: thesis: ( not x in proj1 (X --> L) or (X --> L) . x is 1-sorted )
set IT = X --> L;
assume x in dom (X --> L) ; :: thesis: (X --> L) . x is 1-sorted
then (X --> L) . x in rng (X --> L) by FUNCT_1:def 3;
hence (X --> L) . x is 1-sorted by TARSKI:def 1; :: thesis: verum