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 ) )
proof
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 ) )
proof
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;
assume that
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;
dom (b .--> a) = {b}
.= rng (a .--> b) by FUNCOP_1:8 ;
hence (a .--> b) " = b .--> a by A1, FUNCT_1:32; :: thesis: verum