rng ((T,x) <- T9) c= D
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((T,x) <- T9) or y in D )
assume y in rng ((T,x) <- T9) ; :: thesis: y in D
then consider z being object such that
A1: z in dom ((T,x) <- T9) and
A2: y = ((T,x) <- T9) . z by FUNCT_1:def 3;
reconsider z = z as Node of ((T,x) <- T9) by A1;
reconsider p9 = {} as Node of T9 by TREES_1:22;
per cases ( z in dom T or ex q being Node of T ex r being Node of T9 st
( q in Leaves (dom T) & T . q = x & z = q ^ r ) ) by Def7;
suppose z in dom T ; :: thesis: y in D
then reconsider p = z as Node of T ;
hereby :: thesis: verum
per cases ( ( p in Leaves (dom T) & T . p = x ) or not p in Leaves (dom T) or T . p <> x ) ;
suppose ( p in Leaves (dom T) & T . p = x ) ; :: thesis: y in D
then A3: ((T,x) <- T9) . (p ^ p9) = T9 . p9 by Def7;
p ^ p9 = p by FINSEQ_1:34;
hence y in D by A2, A3; :: thesis: verum
end;
suppose ( not p in Leaves (dom T) or T . p <> x ) ; :: thesis: y in D
then ((T,x) <- T9) . p = T . p by Def7;
hence y in D by A2; :: thesis: verum
end;
end;
end;
end;
suppose ex q being Node of T ex r being Node of T9 st
( q in Leaves (dom T) & T . q = x & z = q ^ r ) ; :: thesis: y in D
then consider q being Node of T, r being Node of T9 such that
A4: ( q in Leaves (dom T) & T . q = x & z = q ^ r ) ;
((T,x) <- T9) . z = T9 . r by A4, Def7;
hence y in D by A2; :: thesis: verum
end;
end;
end;
hence (T,x) <- T9 is D -valued by RELAT_1:def 19; :: thesis: verum