A2: for k being Nat st k in dom p holds
p . k = ({} ^ p) . k

proof

let k be Nat; :: thesis: ( k in dom p implies p . k = ({} ^ p) . k )
assume A3: k in dom p ; :: thesis: p . k = ({} ^ p) . k
thus ({} ^ p) . k = ({} ^ p) . ((len {}) + k)
.= p . k by A3, Def3 ; :: thesis: verum

end;

dom ({} ^ p) = (len {}) + (len p) by Def3
.= dom p ;
hence {} ^ p = p by A2; :: thesis: verum