let x, y be object ; :: 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: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 :: thesis: 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*>) . z

let z be object ; :: 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 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;
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; :: thesis: verum

end;

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