let p be FinSequence; :: thesis: ( p ^ {} = p & {} ^ p = p )
dom (p ^ {}) = Seg (len (p ^ {})) by Def3
.= Seg ((len p) + (len {})) by Th22
.= dom p by Def3 ;
hence p ^ {} = p by Def7; :: thesis: {} ^ p = p
A2: dom ({} ^ p) = Seg (len ({} ^ p)) by Def3
.= Seg ((len {}) + (len p)) by Th22
.= dom p by Def3 ;
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, Def7 ; :: thesis: verum

end;

hence {} ^ p = p by A2; :: thesis: verum