let CS be CongrSpace; 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; ( f is_DIL_of CS & g is_DIL_of CS implies f * g is_DIL_of CS )
A1:
now 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 CSlet a,
b,
x,
y,
z,
t be
Element of
CS;
( [[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
;
[[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;
verum end;
A4:
now for x, y, z being Element of CS holds [[x,x],[y,z]] in the CONGR of CSlet x,
y,
z be
Element of
CS;
[[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;
verum end;
assume
( f is_DIL_of CS & g is_DIL_of CS )
; 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
; verum