let w be Element of Args (o,T); :: thesis: w is Union the Sorts of T -valued
let a be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not a in proj2 w or a in Union the Sorts of T )
reconsider b = a as set by TARSKI:1;
assume a in rng w ; :: thesis: a in Union the Sorts of T
then consider i being object such that
A1: ( i in dom w & b = w . i ) by FUNCT_1:def 3;
reconsider i = i as Nat by A1;
dom w = dom (the_arity_of o) by MSUALG_6:2;
then a is Element of the Sorts of T . ((the_arity_of o) /. i) by A1, MSUALG_6:2;
hence a in Union the Sorts of T ; :: thesis: verum