A1: for k being Nat st k in dom p holds
p . k = (p ^ {}) . k by Def3;
dom (p ^ {}) = (len p) + (len {}) by Def3
.= dom p ;
hence p ^ {} = p by A1; :: thesis: verum