set xH = { (h . x) where h is Permutation of Q : h in Mlt H } ;
{ (h . x) where h is Permutation of Q : h in Mlt H } c= the carrier of Q

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (h . x) where h is Permutation of Q : h in Mlt H } or y in the carrier of Q )
assume y in { (h . x) where h is Permutation of Q : h in Mlt H } ; :: thesis: y in the carrier of Q
then ex h being Permutation of Q st
( y = h . x & h in Mlt H ) ;
hence y in the carrier of Q ; :: thesis: verum

end;

then reconsider xH = { (h . x) where h is Permutation of Q : h in Mlt H } as Subset of Q ;
take xH ; :: thesis: for y being Element of Q holds
( y in xH iff ex h being Permutation of Q st
( h in Mlt H & y = h . x ) )
let y be Element of Q; :: thesis: ( y in xH iff ex h being Permutation of Q st
( h in Mlt H & y = h . x ) )
( y in xH implies ex h being Permutation of Q st
( h in Mlt H & y = h . x ) )

proof

assume y in xH ; :: thesis: ex h being Permutation of Q st
( h in Mlt H & y = h . x )
then ex h being Permutation of Q st
( y = h . x & h in Mlt H ) ;
hence ex h being Permutation of Q st
( h in Mlt H & y = h . x ) ; :: thesis: verum

end;

hence ( y in xH iff ex h being Permutation of Q st
( h in Mlt H & y = h . x ) ) ; :: thesis: verum