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 ) ;
OAS is CongrSpace by Th26;
then f * g is_DIL_of OAS by A1, Th25;
hence f * g is positive_dilatation ; :: thesis: verum