let AS be non empty AffinStruct ; :: thesis: 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; :: thesis: ( f is_DIL_of AS iff for a, b being Element of AS holds a,b // f . a,f . b )

A1: now

assume f is_DIL_of AS ; :: thesis: for a, b being Element of AS holds a,b // f . a,f . b
then A2: f is_FormalIz_of the CONGR of AS by Def4;
let a, b be Element of AS; :: thesis: a,b // f . a,f . b
[[a,b],[(f . a),(f . b)]] in the CONGR of AS by A2, Def2;
hence a,b // f . a,f . b by ANALOAF:def 2; :: thesis: verum

end;

now

assume A3: for a, b being Element of AS holds a,b // f . a,f . b ; :: thesis: f is_DIL_of AS
for x, y being Element of AS holds [[x,y],[(f . x),(f . y)]] in the CONGR of AS

proof

let x, y be Element of AS; :: thesis: [[x,y],[(f . x),(f . y)]] in the CONGR of AS
x,y // f . x,f . y by A3;
hence [[x,y],[(f . x),(f . y)]] in the CONGR of AS by ANALOAF:def 2; :: thesis: verum

end;

then f is_FormalIz_of the CONGR of AS by Def2;
hence f is_DIL_of AS by Def4; :: thesis: 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; :: thesis: verum