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 x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {f} ^ {g} or x in {(f ^ g)} )
assume x in {f} ^ {g} ; :: thesis: x in {(f ^ g)}
then consider p, q being FinSequence such that
A1: ( x = p ^ q & p in {f} & q in {g} ) by POLNOT_1:def 2;
( p = f & q = g ) by A1, TARSKI:def 1;
hence x in {(f ^ g)} by A1, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(f ^ g)} or x in {f} ^ {g} )
A2: ( f in {f} & g in {g} ) by TARSKI:def 1;
assume x in {(f ^ g)} ; :: thesis: x in {f} ^ {g}
then x = f ^ g by TARSKI:def 1;
hence x in {f} ^ {g} by A2, POLNOT_1:def 2; :: thesis: verum