let OAS be OAffinSpace; :: thesis: for a, b being Element of OAS

for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds

f = g

let a, b be Element of OAS; :: thesis: for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds

f = g

let f, g be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b implies f = g )

assume that

A1: f is dilatation and

A2: g is dilatation and

A3: f . a = g . a and

A4: f . b = g . b ; :: thesis: ( a = b or f = g )

A5: ((g ") * f) . b = (g ") . (g . b) by A4, FUNCT_2:15

.= b by Th2 ;

A6: g " is dilatation by A2, Th43;

assume A7: a <> b ; :: thesis: f = g

((g ") * f) . a = (g ") . (g . a) by A3, FUNCT_2:15

.= a by Th2 ;

then A8: (g ") * f = id the carrier of OAS by A1, A7, A5, A6, Th44, Th51;

for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds

f = g

let a, b be Element of OAS; :: thesis: for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds

f = g

let f, g be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b implies f = g )

assume that

A1: f is dilatation and

A2: g is dilatation and

A3: f . a = g . a and

A4: f . b = g . b ; :: thesis: ( a = b or f = g )

A5: ((g ") * f) . b = (g ") . (g . b) by A4, FUNCT_2:15

.= b by Th2 ;

A6: g " is dilatation by A2, Th43;

assume A7: a <> b ; :: thesis: f = g

((g ") * f) . a = (g ") . (g . a) by A3, FUNCT_2:15

.= a by Th2 ;

then A8: (g ") * f = id the carrier of OAS by A1, A7, A5, A6, Th44, Th51;

now :: thesis: for x being Element of OAS holds g . x = f . x

hence
f = g
by FUNCT_2:63; :: thesis: verumlet x be Element of OAS; :: thesis: g . x = f . x

(g ") . (f . x) = ((g ") * f) . x by FUNCT_2:15;

then (g ") . (f . x) = x by A8;

hence g . x = f . x by Th2; :: thesis: verum

end;(g ") . (f . x) = ((g ") * f) . x by FUNCT_2:15;

then (g ") . (f . x) = x by A8;

hence g . x = f . x by Th2; :: thesis: verum