consider n being natural number such that
A3: ord a = p |^ n by def1;
consider m being natural number such that
A4: ord b = p |^ m by def1;
A5: a |^ (p |^ (n + m)) = a |^ ((p |^ n) * (p |^ m)) by NEWTON:13
.= (a |^ (p |^ n)) |^ (p |^ m) by GROUP_1:67
.= (1_ G) |^ (p |^ m) by A3, GROUP_1:82
.= 1_ G by GROUP_1:61 ;
b |^ (p |^ (n + m)) = b |^ ((p |^ m) * (p |^ n)) by NEWTON:13
.= (b |^ (p |^ m)) |^ (p |^ n) by GROUP_1:67
.= (1_ G) |^ (p |^ n) by A4, GROUP_1:82
.= 1_ G by GROUP_1:61 ;
then (a * b) |^ (p |^ (n + m)) = (1_ G) * (1_ G) by A5, GROUP_1:96
.= 1_ G by GROUP_1:def 5 ;
then consider r being natural number such that
A7: ( ord (a * b) = p |^ r & r <= n + m ) by GROUP_1:86, Th2;
take r ; :: according to GROUPP_1:def 1 :: thesis: ord (a * b) = p |^ r
thus ord (a * b) = p |^ r by A7; :: thesis: verum