let V be non empty set ; :: thesis: for W being non empty Subset of V
for A, B being Element of W
for A', B' being Element of V st A = A' & B = B' holds
Maps A,B = Maps A',B'
let W be non empty Subset of V; :: thesis: for A, B being Element of W
for A', B' being Element of V st A = A' & B = B' holds
Maps A,B = Maps A',B'
let A, B be Element of W; :: thesis: for A', B' being Element of V st A = A' & B = B' holds
Maps A,B = Maps A',B'
let A', B' be Element of V; :: thesis: ( A = A' & B = B' implies Maps A,B = Maps A',B' )
assume A1:
( A = A' & B = B' )
; :: thesis: Maps A,B = Maps A',B'
now let x be
set ;
:: thesis: ( ( x in Maps A,B implies x in Maps A',B' ) & ( x in Maps A',B' implies x in Maps A,B ) )thus
(
x in Maps A,
B implies
x in Maps A',
B' )
:: thesis: ( x in Maps A',B' 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 A',B'
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 m' =
x as
Element of
Maps V by A2;
A6:
(
dom m = dom m' &
cod m = cod m' )
;
m = [[A,B],(m `2 )]
by A3, Th16;
then
(
dom m = A &
cod m = B )
by A5, Lm1;
hence
x in Maps A',
B'
by A1, A6, Th19;
:: thesis: verum
end; assume A7:
x in Maps A',
B'
;
:: thesis: x in Maps A,B
Maps A',
B' c= Maps V
by Th17;
then reconsider m' =
x as
Element of
Maps V by A7;
A8:
m' = [[A',B'],(m' `2 )]
by A7, Th16;
then A9:
m' `2 is
Function of
A',
B'
by A7, Lm4;
(
B' = {} implies
A' = {} )
by A7, A8, Lm4;
hence
x in Maps A,
B
by A1, A8, A9, Th15;
:: thesis: verum end;
hence
Maps A,B = Maps A',B'
by TARSKI:2; :: thesis: verum