let V be non empty set ; :: thesis: for W being non empty Subset of V
for A, B being Element of W
for A9, B9 being Element of V st A = A9 & B = B9 holds
Maps (A,B) = Maps (A9,B9)
let W be non empty Subset of V; :: thesis: for A, B being Element of W
for A9, B9 being Element of V st A = A9 & B = B9 holds
Maps (A,B) = Maps (A9,B9)
let A, B be Element of W; :: thesis: for A9, B9 being Element of V st A = A9 & B = B9 holds
Maps (A,B) = Maps (A9,B9)
let A9, B9 be Element of V; :: thesis: ( A = A9 & B = B9 implies Maps (A,B) = Maps (A9,B9) )
assume A1: ( A = A9 & B = B9 ) ; :: thesis: Maps (A,B) = Maps (A9,B9)

now :: thesis: for x being object holds
( ( x in Maps (A,B) implies x in Maps (A9,B9) ) & ( x in Maps (A9,B9) implies x in Maps (A,B) ) )

let x be object ; :: thesis: ( ( x in Maps (A,B) implies x in Maps (A9,B9) ) & ( x in Maps (A9,B9) implies x in Maps (A,B) ) )
thus ( x in Maps (A,B) implies x in Maps (A9,B9) ) :: thesis: ( x in Maps (A9,B9) implies x in Maps (A,B) )

proof

A2: Maps W c= Maps V by Th7;
assume A3: x in Maps (A,B) ; :: thesis: x in Maps (A9,B9)
A4: Maps (A,B) c= Maps W by Th17;
then reconsider m = x as Element of Maps W by A3;
x in Maps W by A3, A4;
then reconsider m9 = x as Element of Maps V by A2;
A5: ( dom m = dom m9 & cod m = cod m9 ) ;
m = [[A,B],(m `2)] by A3, Th16;
then ( dom m = A & cod m = B ) ;
hence x in Maps (A9,B9) by A1, A5, Th19; :: thesis: verum

end;

assume A6: x in Maps (A9,B9) ; :: thesis: x in Maps (A,B)
Maps (A9,B9) c= Maps V by Th17;
then reconsider m9 = x as Element of Maps V by A6;
A7: m9 = [[A9,B9],(m9 `2)] by A6, Th16;
then A8: m9 `2 is Function of A9,B9 by A6, Lm4;
( B9 = {} implies A9 = {} ) by A6, A7, Lm4;
hence x in Maps (A,B) by A1, A7, A8, Th15; :: thesis: verum

end;

hence Maps (A,B) = Maps (A9,B9) by TARSKI:2; :: thesis: verum