let V be non empty set ; 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; 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; 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; ( A = A9 & B = B9 implies Maps (A,B) = Maps (A9,B9) )
assume A1:
( A = A9 & B = B9 )
; Maps (A,B) = Maps (A9,B9)
now 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 ;
( ( 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) )
( 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)
;
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;
verum
end; assume A6:
x in Maps (
A9,
B9)
;
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;
verum end;
hence
Maps (A,B) = Maps (A9,B9)
by TARSKI:2; verum