let OAS be OAffinSpace; :: thesis: for f, g being Permutation of the carrier of OAS st f is positive_dilatation & g is positive_dilatation holds
f * g is positive_dilatation
let f, g be Permutation of the carrier of OAS; :: thesis: ( f is positive_dilatation & g is positive_dilatation implies f * g is positive_dilatation )
assume ( f is positive_dilatation & g is positive_dilatation ) ; :: thesis: f * g is positive_dilatation
then A1: ( f is_DIL_of OAS & g is_DIL_of OAS ) by Def6;
OAS is CongrSpace by Th40;
then f * g is_DIL_of OAS by A1, Th39;
hence f * g is positive_dilatation by Def6; :: thesis: verum