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

let x be set ; :: 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;
A5: m = [[(dom m),(cod m)],(m `2)] by Th8;
x in Maps W by A3, A4;
then reconsider m9 = x as Element of Maps V by A2;
A6: ( dom m = dom m9 & cod m = cod m9 ) ;
m = [[A,B],(m `2)] by A3, Th16;
then ( dom m = A & cod m = B ) by A5, Lm1;
hence x in Maps (A9,B9) by A1, A6, Th19; :: thesis: verum

end;

assume A7: 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 A7;
A8: m9 = [[A9,B9],(m9 `2)] by A7, Th16;
then A9: m9 `2 is Function of A9,B9 by A7, Lm4;
( B9 = {} implies A9 = {} ) by A7, A8, Lm4;
hence x in Maps (A,B) by A1, A8, A9, Th15; :: thesis: verum

end;

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