let x, y be object ; 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:40
;
A2:
dom (root-tree y) = elementary_tree 0
;
A3:
( dom ((elementary_tree 1) --> x) = elementary_tree 1 & <*0*> in elementary_tree 1 )
by TARSKI:def 2, TREES_1:51;
then A4: dom (((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) =
(elementary_tree 1) with-replacement (<*0*>,(elementary_tree 0))
by A2, TREES_2:def 11
.=
elementary_tree 1
by TREES_3:58, TREES_3:67
;
now for z being object st z in elementary_tree 1 holds
(((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) . z = (x -flat_tree <*y*>) . zlet z be
object ;
( 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
;
(((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) . z = (x -flat_tree <*y*>) . zthen A5:
(
z = {} or
z = <*0*> )
by TARSKI:def 2, TREES_1:51;
A6:
{} in elementary_tree 1
by TARSKI:def 2, TREES_1:51;
A7:
not
<*0*> is_a_prefix_of {}
;
A8:
len <*y*> = 1
by FINSEQ_1:40;
A9:
(
<*y*> . 1
= y &
(x -flat_tree <*y*>) . {} = x )
by Def3, FINSEQ_1:40;
A10:
(((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) . {} = ((elementary_tree 1) --> x) . {}
by A3, A6, A7, TREES_3:45;
A11:
(x -flat_tree <*y*>) . <*0*> = <*y*> . (0 + 1)
by A8, Def3;
(((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) . <*0*> = (root-tree y) . {}
by A3, TREES_3:44;
hence
(((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) . z = (x -flat_tree <*y*>) . z
by A5, A6, A9, A10, A11, Th3, FUNCOP_1:7;
verum end;
hence
x -flat_tree <*y*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))
by A1, A4; verum