let p be XFinSequence; :: thesis: ( p ^ {} = p & {} ^ p = p )
A1: for k being Nat st k in dom p holds
p . k = (p ^ {}) . k by Def4;
dom (p ^ {}) = (len p) + (len {}) by Def4
.= dom p ;
hence p ^ {} = p by A1, Th10; :: thesis: {} ^ p = p
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, Def4 ; :: thesis: verum

end;

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