set f = root-tree x;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 (root-tree x) or not x2 in proj1 (root-tree x) or not (root-tree x) . x1 = (root-tree x) . x2 or x1 = x2 )
assume ( x1 in dom (root-tree x) & x2 in dom (root-tree x) & (root-tree x) . x1 = (root-tree x) . x2 ) ; :: thesis: x1 = x2
then ( x1 = {} & x2 = {} ) by TREES_1:29, TARSKI:def 1;
hence x1 = x2 ; :: thesis: verum