let OAS be OAffinSpace; for f being Permutation of the carrier of OAS st f is dilatation holds
for a, b, c, d being Element of OAS holds
( a,b '||' c,d iff f . a,f . b '||' f . c,f . d )
let f be Permutation of the carrier of OAS; ( f is dilatation implies for a, b, c, d being Element of OAS holds
( a,b '||' c,d iff f . a,f . b '||' f . c,f . d ) )
assume A1:
f is dilatation
; for a, b, c, d being Element of OAS holds
( a,b '||' c,d iff f . a,f . b '||' f . c,f . d )
let a, b, c, d be Element of OAS; ( a,b '||' c,d iff f . a,f . b '||' f . c,f . d )
A2:
c,d '||' f . c,f . d
by A1, Th34;
A3:
a,b '||' f . a,f . b
by A1, Th34;
A4:
now ( f . a,f . b '||' f . c,f . d implies a,b '||' c,d )A5:
now ( a,b '||' f . c,f . d implies a,b '||' c,d )A6:
now ( f . c = f . d implies a,b '||' c,d )end; assume
a,
b '||' f . c,
f . d
;
a,b '||' c,dhence
a,
b '||' c,
d
by A2, A6, DIRAF:23;
verum A7:
now ( f . a = f . b implies a,b '||' c,d )end; assume
f . a,
f . b '||' f . c,
f . d
;
a,b '||' c,dhence
a,
b '||' c,
d
by A3, A7, A5, DIRAF:23;
verum
now ( a,b '||' c,d implies f . a,f . b '||' f . c,f . d )A8:
now ( f . a,f . b '||' c,d implies f . a,f . b '||' f . c,f . d )A9:
(
c = d implies
f . a,
f . b '||' f . c,
f . d )
by DIRAF:20;
assume
f . a,
f . b '||' c,
d
;
f . a,f . b '||' f . c,f . dhence
f . a,
f . b '||' f . c,
f . d
by A2, A9, DIRAF:23;
verum end; assume
a,
b '||' c,
d
;
f . a,f . b '||' f . c,f . dthen
(
f . a,
f . b '||' c,
d or
a = b )
by A3, DIRAF:23;
hence
f . a,
f . b '||' f . c,
f . d
by A8, DIRAF:20;
verum
hence
( a,b '||' c,d iff f . a,f . b '||' f . c,f . d )
by A4; verum