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: ( ( for x being object st x in dom IT holds
IT . x is 1-sorted ) implies IT is 1-sorted-yielding )
assume A2: for x being object st x in dom IT holds
IT . x is 1-sorted ; :: thesis: IT is 1-sorted-yielding
for x being object st x in rng IT holds
x is 1-sorted

proof

let x be object ; :: thesis: ( x in rng IT implies x is 1-sorted )
assume x in rng IT ; :: thesis: x is 1-sorted
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: verum

end;

hence IT is 1-sorted-yielding ; :: thesis: verum