let x, y be set ; :: thesis: x -flat_tree <*y*> = ((elementary_tree 1) --> x) with-replacement <*0 *>,(root-tree y)
set T = ((elementary_tree 1) --> x) with-replacement <*0 *>,(root-tree y);
A1: dom (x -flat_tree <*y*>) =
elementary_tree (len <*y*>)
by Def3
.=
elementary_tree 1
by FINSEQ_1:57
;
A2:
( dom ((elementary_tree 1) --> x) = elementary_tree 1 & dom (root-tree y) = elementary_tree 0 & <*0 *> in elementary_tree 1 )
by FUNCOP_1:19, TARSKI:def 2, TREES_1:88;
then A3: dom (((elementary_tree 1) --> x) with-replacement <*0 *>,(root-tree y)) =
(elementary_tree 1) with-replacement <*0 *>,(elementary_tree 0 )
by TREES_2:def 12
.=
elementary_tree 1
by TREES_3:61, TREES_3:70
;
now let z be
set ;
:: thesis: ( z in elementary_tree 1 implies (((elementary_tree 1) --> x) with-replacement <*0 *>,(root-tree y)) . z = (x -flat_tree <*y*>) . z )assume
z in elementary_tree 1
;
:: thesis: (((elementary_tree 1) --> x) with-replacement <*0 *>,(root-tree y)) . z = (x -flat_tree <*y*>) . zthen A4:
( (
z = {} or
z = <*0 *> ) &
{} in elementary_tree 1 &
<*0 *> in elementary_tree 1 )
by TARSKI:def 2, TREES_1:88;
A5:
( not
<*0 *> is_a_prefix_of {} &
len <*y*> = 1 &
0 < 1 &
<*y*> . 1
= y )
by FINSEQ_1:57;
then
(
(x -flat_tree <*y*>) . {} = x &
(((elementary_tree 1) --> x) with-replacement <*0 *>,(root-tree y)) . {} = ((elementary_tree 1) --> x) . {} &
((elementary_tree 1) --> x) . {} = x &
(x -flat_tree <*y*>) . <*0 *> = <*y*> . (0 + 1) &
(((elementary_tree 1) --> x) with-replacement <*0 *>,(root-tree y)) . <*0 *> = (root-tree y) . {} )
by A2, A4, Def3, FUNCOP_1:13, TREES_3:47, TREES_3:48;
hence
(((elementary_tree 1) --> x) with-replacement <*0 *>,(root-tree y)) . z = (x -flat_tree <*y*>) . z
by A4, A5, Th3;
:: thesis: verum end;
hence
x -flat_tree <*y*> = ((elementary_tree 1) --> x) with-replacement <*0 *>,(root-tree y)
by A1, A3, FUNCT_1:9; :: thesis: verum