let a, b be set ; :: thesis: (a .--> b) " = b .--> a

set f = a .--> b;

set g = b .--> a;

A1: for y, x being object holds

( y in rng (a .--> b) & x = (b .--> a) . y iff ( x in dom (a .--> b) & y = (a .--> b) . x ) )

.= rng (a .--> b) by FUNCOP_1:8 ;

hence (a .--> b) " = b .--> a by A1, FUNCT_1:32; :: thesis: verum

set f = a .--> b;

set g = b .--> a;

A1: for y, x being object holds

( y in rng (a .--> b) & x = (b .--> a) . y iff ( x in dom (a .--> b) & y = (a .--> b) . x ) )

proof

dom (b .--> a) =
{b}
let y, x be object ; :: thesis: ( y in rng (a .--> b) & x = (b .--> a) . y iff ( x in dom (a .--> b) & y = (a .--> b) . x ) )

thus ( y in rng (a .--> b) & x = (b .--> a) . y implies ( x in dom (a .--> b) & y = (a .--> b) . x ) ) :: thesis: ( x in dom (a .--> b) & y = (a .--> b) . x implies ( y in rng (a .--> b) & x = (b .--> a) . y ) )

A7: x in dom (a .--> b) and

A8: y = (a .--> b) . x ; :: thesis: ( y in rng (a .--> b) & x = (b .--> a) . y )

A9: x in {a} by A7;

then A10: y = (a .--> b) . a by A8, TARSKI:def 1

.= b by FUNCOP_1:72 ;

then A11: y in {b} by TARSKI:def 1;

(b .--> a) . y = a by A10, FUNCOP_1:72

.= x by A9, TARSKI:def 1 ;

hence ( y in rng (a .--> b) & x = (b .--> a) . y ) by A11, FUNCOP_1:8; :: thesis: verum

end;thus ( y in rng (a .--> b) & x = (b .--> a) . y implies ( x in dom (a .--> b) & y = (a .--> b) . x ) ) :: thesis: ( x in dom (a .--> b) & y = (a .--> b) . x implies ( y in rng (a .--> b) & x = (b .--> a) . y ) )

proof

assume that
assume that

A2: y in rng (a .--> b) and

A3: x = (b .--> a) . y ; :: thesis: ( x in dom (a .--> b) & y = (a .--> b) . x )

A4: y in {b} by A2, FUNCOP_1:8;

then A5: x = (b .--> a) . b by A3, TARSKI:def 1

.= a by FUNCOP_1:72 ;

then A6: x in {a} by TARSKI:def 1;

(a .--> b) . x = b by A5, FUNCOP_1:72

.= y by A4, TARSKI:def 1 ;

hence ( x in dom (a .--> b) & y = (a .--> b) . x ) by A6; :: thesis: verum

end;A2: y in rng (a .--> b) and

A3: x = (b .--> a) . y ; :: thesis: ( x in dom (a .--> b) & y = (a .--> b) . x )

A4: y in {b} by A2, FUNCOP_1:8;

then A5: x = (b .--> a) . b by A3, TARSKI:def 1

.= a by FUNCOP_1:72 ;

then A6: x in {a} by TARSKI:def 1;

(a .--> b) . x = b by A5, FUNCOP_1:72

.= y by A4, TARSKI:def 1 ;

hence ( x in dom (a .--> b) & y = (a .--> b) . x ) by A6; :: thesis: verum

A7: x in dom (a .--> b) and

A8: y = (a .--> b) . x ; :: thesis: ( y in rng (a .--> b) & x = (b .--> a) . y )

A9: x in {a} by A7;

then A10: y = (a .--> b) . a by A8, TARSKI:def 1

.= b by FUNCOP_1:72 ;

then A11: y in {b} by TARSKI:def 1;

(b .--> a) . y = a by A10, FUNCOP_1:72

.= x by A9, TARSKI:def 1 ;

hence ( y in rng (a .--> b) & x = (b .--> a) . y ) by A11, FUNCOP_1:8; :: thesis: verum

.= rng (a .--> b) by FUNCOP_1:8 ;

hence (a .--> b) " = b .--> a by A1, FUNCT_1:32; :: thesis: verum