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 ;

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

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

end;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, 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; :: thesis: verum