let xH1, xH2 be Subset of Q; :: thesis: ( ( for y being Element of Q holds
( y in xH1 iff ex h being Permutation of Q st
( h in Mlt H & y = h . x ) ) ) & ( for y being Element of Q holds
( y in xH2 iff ex h being Permutation of Q st
( h in Mlt H & y = h . x ) ) ) implies xH1 = xH2 )
assume that
A1: for y being Element of Q holds
( y in xH1 iff ex h being Permutation of Q st
( h in Mlt H & y = h . x ) ) and
A2: for y being Element of Q holds
( y in xH2 iff ex h being Permutation of Q st
( h in Mlt H & y = h . x ) ) ; :: thesis: xH1 = xH2
for y being Element of Q holds
( y in xH1 iff y in xH2 )
proof
let y be Element of Q; :: thesis: ( y in xH1 iff y in xH2 )
( y in xH1 iff ex h being Permutation of Q st
( h in Mlt H & y = h . x ) ) by A1;
hence ( y in xH1 iff y in xH2 ) by A2; :: thesis: verum
end;
hence xH1 = xH2 by SUBSET_1:3; :: thesis: verum