consider n being Nat such that
A1: ord a = p |^ n by Def1;
consider m being Nat such that
A2: ord b = p |^ m by Def1;
A3: a |^ (p |^ (n + m)) = a |^ ((p |^ n) * (p |^ m)) by NEWTON:8
.= (a |^ (p |^ n)) |^ (p |^ m) by GROUP_1:35
.= (1_ G) |^ (p |^ m) by A1, GROUP_1:41
.= 1_ G by GROUP_1:31 ;
b |^ (p |^ (n + m)) = b |^ ((p |^ m) * (p |^ n)) by NEWTON:8
.= (b |^ (p |^ m)) |^ (p |^ n) by GROUP_1:35
.= (1_ G) |^ (p |^ n) by A2, GROUP_1:41
.= 1_ G by GROUP_1:31 ;
then (a * b) |^ (p |^ (n + m)) = (1_ G) * (1_ G) by A3, GROUP_1:48
.= 1_ G by GROUP_1:def 4 ;
then consider r being Nat such that
A4: ( ord (a * b) = p |^ r & r <= n + m ) by Th2, GROUP_1:44;
take r ; :: according to GROUPP_1:def 1 :: thesis: ord (a * b) = p |^ r
thus ord (a * b) = p |^ r by A4; :: thesis: verum