let AS be non empty AffinStruct ; for f being Permutation of the carrier of AS holds
( f is_DIL_of AS iff for a, b being Element of AS holds a,b // f . a,f . b )
let f be Permutation of the carrier of AS; ( f is_DIL_of AS iff for a, b being Element of AS holds a,b // f . a,f . b )
now ( f is_DIL_of AS implies for a, b being Element of AS holds a,b // f . a,f . b )assume A3:
f is_DIL_of AS
;
for a, b being Element of AS holds a,b // f . a,f . blet a,
b be
Element of
AS;
a,b // f . a,f . b
f is_FormalIz_of the
CONGR of
AS
by A3;
then
[[a,b],[(f . a),(f . b)]] in the
CONGR of
AS
;
hence
a,
b // f . a,
f . b
by ANALOAF:def 2;
verum end;
hence
( f is_DIL_of AS iff for a, b being Element of AS holds a,b // f . a,f . b )
by A1; verum