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

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