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 ;
then A5: x = (b .--> a) . b by
.= a by FUNCOP_1:72 ;
then A6: x in {a} by TARSKI:def 1;
(a .--> b) . x = b by
.= y by ;
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
.= b by FUNCOP_1:72 ;
then A11: y in {b} by TARSKI:def 1;
(b .--> a) . y = a by
.= x by ;
hence ( y in rng (a .--> b) & x = (b .--> a) . y ) by ; :: thesis: verum
end;
dom (b .--> a) = {b}
.= rng (a .--> b) by FUNCOP_1:8 ;
hence (a .--> b) " = b .--> a by ; :: thesis: verum