let V be non empty set ; :: thesis: for W being non empty Subset of
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 ; :: 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