let x, y be object ; :: thesis: x -flat_tree <*y*> = (() --> x) with-replacement (,())
set T = (() --> x) with-replacement (,());
A1: dom () = elementary_tree () by Def3
.= elementary_tree 1 by FINSEQ_1:40 ;
A2: dom () = elementary_tree 0 ;
A3: ( dom (() --> x) = elementary_tree 1 & in elementary_tree 1 ) by ;
then A4: dom ((() --> x) with-replacement (,())) = () with-replacement (,) by
.= elementary_tree 1 by ;
now :: thesis: for z being object st z in elementary_tree 1 holds
((() --> x) with-replacement (,())) . z = () . z
let z be object ; :: thesis: ( z in elementary_tree 1 implies ((() --> x) with-replacement (,())) . z = () . z )
assume z in elementary_tree 1 ; :: thesis: ((() --> x) with-replacement (,())) . z = () . z
then A5: ( z = {} or z = ) by ;
A6: {} in elementary_tree 1 by ;
A7: not <*0*> is_a_prefix_of {} ;
A8: len <*y*> = 1 by FINSEQ_1:40;
A9: ( <*y*> . 1 = y & () . {} = x ) by ;
A10: (((elementary_tree 1) --> x) with-replacement (,())) . {} = (() --> x) . {} by ;
A11: (x -flat_tree <*y*>) . = <*y*> . (0 + 1) by ;
(((elementary_tree 1) --> x) with-replacement (,())) . = () . {} by ;
hence (((elementary_tree 1) --> x) with-replacement (,())) . z = () . z by ; :: thesis: verum
end;
hence x -flat_tree <*y*> = (() --> x) with-replacement (,()) by A1, A4; :: thesis: verum