let x be object ; :: thesis: for g being Function holds pi ({g},x) = {(g . x)}
let g be Function; :: thesis: pi ({g},x) = {(g . x)}
thus pi ({g},x) c= {(g . x)} :: according to XBOOLE_0:def 10 :: thesis: {(g . x)} c= pi ({g},x)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in pi ({g},x) or y in {(g . x)} )
assume y in pi ({g},x) ; :: thesis: y in {(g . x)}
then consider f being Function such that
A1: f in {g} and
A2: y = f . x by Def6;
f = g by A1, TARSKI:def 1;
hence y in {(g . x)} by A2, TARSKI:def 1; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {(g . x)} or y in pi ({g},x) )
assume A3: y in {(g . x)} ; :: thesis: y in pi ({g},x)
A4: g in {g} by TARSKI:def 1;
y = g . x by A3, TARSKI:def 1;
hence y in pi ({g},x) by A4, Def6; :: thesis: verum