let CS be CongrSpace; :: thesis: for f, g being Permutation of the carrier of CS st f is_DIL_of CS & g is_DIL_of CS holds
f * g is_DIL_of CS
let f, g be Permutation of the carrier of CS; :: thesis: ( f is_DIL_of CS & g is_DIL_of CS implies f * g is_DIL_of CS )

A1: now :: thesis: for a, b, x, y, z, t being Element of CS st [[x,y],[a,b]] in the CONGR of CS & [[a,b],[z,t]] in the CONGR of CS & a <> b holds
[[x,y],[z,t]] in the CONGR of CS

let a, b, x, y, z, t be Element of CS; :: thesis: ( [[x,y],[a,b]] in the CONGR of CS & [[a,b],[z,t]] in the CONGR of CS & a <> b implies [[x,y],[z,t]] in the CONGR of CS )
assume that
A2: ( [[x,y],[a,b]] in the CONGR of CS & [[a,b],[z,t]] in the CONGR of CS ) and
A3: a <> b ; :: thesis: [[x,y],[z,t]] in the CONGR of CS
( x,y // a,b & a,b // z,t ) by A2, ANALOAF:def 2;
then x,y // z,t by A3, Def5;
hence [[x,y],[z,t]] in the CONGR of CS by ANALOAF:def 2; :: thesis: verum

end;

A4: now :: thesis: for x, y, z being Element of CS holds [[x,x],[y,z]] in the CONGR of CS

let x, y, z be Element of CS; :: thesis: [[x,x],[y,z]] in the CONGR of CS
x,x // y,z by Def5;
hence [[x,x],[y,z]] in the CONGR of CS by ANALOAF:def 2; :: thesis: verum

end;

assume ( f is_DIL_of CS & g is_DIL_of CS ) ; :: thesis: f * g is_DIL_of CS
then ( f is_FormalIz_of the CONGR of CS & g is_FormalIz_of the CONGR of CS ) ;
then f * g is_FormalIz_of the CONGR of CS by A1, A4, Th15;
hence f * g is_DIL_of CS ; :: thesis: verum