let p be FinSequence; :: thesis: ( p ^ {} = p & {} ^ p = p )
A1: dom (p ^ {} ) = Seg (len (p ^ {} )) by Def3
.= Seg ((len p) + (len {} )) by Th35
.= dom p by Def3 ;
thus p ^ {} = p :: thesis: {} ^ p = p

proof

for k being Nat st k in dom p holds
p . k = (p ^ {} ) . k by Def7;
hence p ^ {} = p by A1, Th17; :: thesis: verum

end;

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

proof

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, Th17; :: thesis: verum

end;