let AFS be AffinSpace; :: thesis: for f being Permutation of the carrier of AFS
for A, C being Subset of AFS st f .: A = f .: C holds
A = C
let f be Permutation of the carrier of AFS; :: thesis: for A, C being Subset of AFS st f .: A = f .: C holds
A = C
let A, C be Subset of AFS; :: thesis: ( f .: A = f .: C implies A = C )
assume A1: f .: A = f .: C ; :: thesis: A = C
now :: thesis: for b being object st b in C holds
b in A
let b be object ; :: thesis: ( b in C implies b in A )
assume A2: b in C ; :: thesis: b in A
then reconsider b9 = b as Element of AFS ;
set y = f . b9;
f . b9 in f .: C by A2, Th90;
then ex a being Element of AFS st
( a in A & f . a = f . b9 ) by A1, Th91;
hence b in A by FUNCT_2:58; :: thesis: verum
end;
then A3: C c= A by TARSKI:def 3;
now :: thesis: for a being object st a in A holds
a in C
let a be object ; :: thesis: ( a in A implies a in C )
assume A4: a in A ; :: thesis: a in C
then reconsider a9 = a as Element of AFS ;
set x = f . a9;
f . a9 in f .: A by A4, Th90;
then ex b being Element of AFS st
( b in C & f . b = f . a9 ) by A1, Th91;
hence a in C by FUNCT_2:58; :: thesis: verum
end;
then A c= C by TARSKI:def 3;
hence A = C by A3, XBOOLE_0:def 10; :: thesis: verum