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 )
assume ( f is_DIL_of CS & g is_DIL_of CS ) ; :: thesis: f * g is_DIL_of CS
then A1: ( f is_FormalIz_of the CONGR of CS & g is_FormalIz_of the CONGR of CS ) by Def4;

A2: now

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 ( [[x,y],[a,b]] in the CONGR of CS & [[a,b],[z,t]] in the CONGR of CS & a <> b ) ; :: thesis: [[x,y],[z,t]] in the CONGR of CS
then ( x,y // a,b & a,b // z,t & a <> b ) by ANALOAF:def 2;
then x,y // z,t by Def5;
hence [[x,y],[z,t]] in the CONGR of CS by ANALOAF:def 2; :: thesis: verum

end;

now

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;

then f * g is_FormalIz_of the CONGR of CS by A1, A2, Th26;
hence f * g is_DIL_of CS by Def4; :: thesis: verum