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)

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) ) )

hence
Maps (A,B) = Maps (A9,B9)
by TARSKI:2; :: thesis: verum( ( 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) )

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;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

assume A6:
x in Maps (A9,B9)
; :: thesis: x in Maps (A,B)
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 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

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