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 let x be
set ;
( ( 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;
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;
verum
end; assume A7:
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 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;
verum end;
hence
Maps A,B = Maps A9,B9
by TARSKI:2; verum