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

hence A = C by A3, XBOOLE_0:def 10; :: thesis: verum

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

then A3:
C c= A
by TARSKI:def 3;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;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

now :: thesis: for a being object st a in A holds

a in C

then
A c= C
by TARSKI:def 3;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;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

hence A = C by A3, XBOOLE_0:def 10; :: thesis: verum