AA: dom (((root-tree c),c) <- d) = dom d

proof

let x be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not x in dom (((root-tree c),c) <- d) or x in dom d ) & ( not x in dom d or x in dom (((root-tree c),c) <- d) ) )

hereby :: thesis: ( not x in dom d or x in dom (((root-tree c),c) <- d) )

assume x in dom (((root-tree c),c) <- d) ; :: thesis: x in dom d
then reconsider p = x as Element of dom (((root-tree c),c) <- d) ;

per cases ( p in dom (root-tree c) or ex q being Node of (root-tree c) ex r being Node of d st
( q in Leaves (dom (root-tree c)) & (root-tree c) . q = c & p = q ^ r ) ) by TREES_4:def 7;

suppose p in dom (root-tree c) ; :: thesis: x in dom d

then p in elementary_tree 0 ;
then p = {} by TREES_1:29;
hence x in dom d by TREES_1:22; :: thesis: verum

end;

suppose ex q being Node of (root-tree c) ex r being Node of d st
( q in Leaves (dom (root-tree c)) & (root-tree c) . q = c & p = q ^ r ) ; :: thesis: x in dom d

then consider q being Node of (root-tree c), r being Node of d such that
A2: ( q in Leaves (dom (root-tree c)) & (root-tree c) . q = c & p = q ^ r ) ;
q in {{}} by TREES_1:29;
then q = {} ;
hence x in dom d by A2; :: thesis: verum

end;

end;

end;

assume x in dom d ; :: thesis: x in dom (((root-tree c),c) <- d)
then reconsider r = x as Node of d ;
reconsider q = {} as Node of (root-tree c) by TREES_1:22;
( q in Leaves (dom (root-tree c)) & (root-tree c) . q = c & r = q ^ r ) by HUFFMAN1:15;
hence x in dom (((root-tree c),c) <- d) by TREES_4:def 7; :: thesis: verum

end;

now :: thesis: for x being object st x in dom d holds
(((root-tree c),c) <- d) . x = d . x

let x be object ; :: thesis: ( x in dom d implies (((root-tree c),c) <- d) . x = d . x )
assume x in dom d ; :: thesis: (((root-tree c),c) <- d) . x = d . x
then reconsider r = x as Node of d ;
reconsider q = {} as Node of (root-tree c) by TREES_1:22;
( q in Leaves (dom (root-tree c)) & (root-tree c) . q = c & r = q ^ r ) by HUFFMAN1:15;
hence (((root-tree c),c) <- d) . x = d . x by TREES_4:def 7; :: thesis: verum

end;

hence ((root-tree c),c) <- d = d by AA, FUNCT_1:2; :: thesis: verum