let P be FinSequence-membered set ; :: thesis: ( P ^ {{}} = P & {{}} ^ P = P )
A1: for a being object holds
( a in P ^ {{}} iff a in P )

proof

let a be object ; :: thesis: ( a in P ^ {{}} iff a in P )
thus ( a in P ^ {{}} implies a in P ) :: thesis: ( a in P implies a in P ^ {{}} )

proof

assume a in P ^ {{}} ; :: thesis: a in P
then consider p, q being FinSequence such that
A2: a = p ^ q and
A3: p in P and
A4: q in {{}} by Def2;
q = {} by A4, TARSKI:def 1;
hence a in P by A2, A3, FINSEQ_1:34; :: thesis: verum

end;

assume A10: a in P ; :: thesis: a in P ^ {{}}
then reconsider a = a as FinSequence ;
{} in {{}} by TARSKI:def 1;
then a ^ {} in P ^ {{}} by A10, Def2;
hence a in P ^ {{}} by FINSEQ_1:34; :: thesis: verum

end;

for a being object holds
( a in {{}} ^ P iff a in P )

proof

let a be object ; :: thesis: ( a in {{}} ^ P iff a in P )
thus ( a in {{}} ^ P implies a in P ) :: thesis: ( a in P implies a in {{}} ^ P )

proof

assume a in {{}} ^ P ; :: thesis: a in P
then consider q, p being FinSequence such that
A12: a = q ^ p and
A13: q in {{}} and
A14: p in P by Def2;
q = {} by A13, TARSKI:def 1;
hence a in P by A12, A14, FINSEQ_1:34; :: thesis: verum

end;

assume A20: a in P ; :: thesis: a in {{}} ^ P
then reconsider a = a as FinSequence ;
{} in {{}} by TARSKI:def 1;
then {} ^ a in {{}} ^ P by A20, Def2;
hence a in {{}} ^ P by FINSEQ_1:34; :: thesis: verum

end;

hence ( P ^ {{}} = P & {{}} ^ P = P ) by A1, TARSKI:2; :: thesis: verum