let f, g be FinSequence; :: thesis: f ^^ {g} = {(f ^ g)}
thus f ^^ {g} c= {(f ^ g)} :: according to XBOOLE_0:def 10 :: thesis: {(f ^ g)} c= f ^^ {g}
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in f ^^ {g} or a in {(f ^ g)} )
assume a in f ^^ {g} ; :: thesis: a in {(f ^ g)}
then consider p being Element of {g} such that
A2: ( a = f ^ p & p in {g} ) ;
p = g by TARSKI:def 1;
hence a in {(f ^ g)} by A2, TARSKI:def 1; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {(f ^ g)} or a in f ^^ {g} )
assume a in {(f ^ g)} ; :: thesis: a in f ^^ {g}
then ( a = f ^ g & g in {g} ) by TARSKI:def 1;
hence a in f ^^ {g} ; :: thesis: verum