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

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

hence
IT is 1-sorted-yielding
; :: thesis: verum
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;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