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 (root-tree y) = elementary_tree 0 by FUNCOP_1:19;
A3: ( dom ((elementary_tree 1) --> x) = elementary_tree 1 & <*0*> in elementary_tree 1 ) by FUNCOP_1:19, TARSKI:def 2, TREES_1:88;
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 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*>) . z
then A7: ( z = {} or z = <*0*> ) by TARSKI:def 2, TREES_1:88;
A8: {} in elementary_tree 1 by TARSKI:def 2, TREES_1:88;
A9: not <*0*> is_a_prefix_of {} ;
A10: len <*y*> = 1 by FINSEQ_1:57;
A11: ( <*y*> . 1 = y & (x -flat_tree <*y*>) . {} = x ) by Def3, FINSEQ_1:57;
A12: (((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) . {} = ((elementary_tree 1) --> x) . {} by A3, A8, A9, TREES_3:48;
A13: (x -flat_tree <*y*>) . <*0*> = <*y*> . (0 + 1) by A10, Def3;
(((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) . <*0*> = (root-tree y) . {} by A3, TREES_3:47;
hence (((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))) . z = (x -flat_tree <*y*>) . z by A7, A8, A11, A12, A13, Th3, FUNCOP_1:13; :: thesis: verum

end;

hence x -flat_tree <*y*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y)) by A1, A4, FUNCT_1:9; :: thesis: verum