let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for g being Element of G
for A being Subset of G holds card A = card (g + A)
let g be Element of G; :: thesis: for A being Subset of G holds card A = card (g + A)
let A be Subset of G; :: thesis: card A = card (g + A)
(- g) + (g + A) = ((- g) + g) + A by Th5
.= (0. G) + A by RLVECT_1:5
.= A by Th6 ;
then A1: card A c= card (g + A) by Lm4;
card (g + A) c= card A by Lm4;
hence card A = card (g + A) by A1; :: thesis: verum