thus ( IT is 1-sorted-yielding implies for x being object st x in dom IT holds
IT . x is 1-sorted ) by FUNCT_1:3; :: thesis:
assume A2: for x being object st x in dom IT holds
IT . x is 1-sorted ; :: thesis:
for x being object st x in rng IT holds
x is 1-sorted

let x be object ; :: thesis:
assume x in rng IT ; :: thesis:
then consider xx being object such that
A3: ( xx in dom IT & x = IT . xx ) by FUNCT_1:def 3;
thus x is 1-sorted by A2, A3; :: thesis:

end;