let V, V', C, C' be set ; :: thesis: for A being Element of Fin (PFuncs V,C)
for B being Element of Fin (PFuncs V',C') st V c= V' & C c= C' & A = B holds
mi A = mi B
let A be Element of Fin (PFuncs V,C); :: thesis: for B being Element of Fin (PFuncs V',C') st V c= V' & C c= C' & A = B holds
mi A = mi B
let B be Element of Fin (PFuncs V',C'); :: thesis: ( V c= V' & C c= C' & A = B implies mi A = mi B )
assume A1: ( V c= V' & C c= C' & A = B ) ; :: thesis: mi A = mi B

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: mi B c= mi A

let x be set ; :: thesis: ( x in mi A implies x in mi B )
assume A2: x in mi A ; :: thesis: x in mi B
then x in { t where t is Element of PFuncs V,C : ( t is finite & ( for s being Element of PFuncs V,C holds
( ( s in A & s c= t ) iff s = t ) ) ) } by SUBSTLAT:def 2;
then consider f being Element of PFuncs V,C such that
A3: ( f = x & f is finite & ( for s being Element of PFuncs V,C holds
( ( s in A & s c= f ) iff s = f ) ) ) ;
A4: x in PFuncs V,C by A3;
PFuncs V,C c= PFuncs V',C' by A1, PARTFUN1:128;
then reconsider f = f as Element of PFuncs V',C' by A3, A4;
for s being Element of PFuncs V',C' holds
( ( s in B & s c= f ) iff s = f ) by A1, A2, A3, SUBSTLAT:6;
then x in { t where t is Element of PFuncs V',C' : ( t is finite & ( for s being Element of PFuncs V',C' holds
( ( s in B & s c= t ) iff s = t ) ) ) } by A3;
hence x in mi B by SUBSTLAT:def 2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in mi B or x in mi A )
assume A5: x in mi B ; :: thesis: x in mi A
then x in { t where t is Element of PFuncs V',C' : ( t is finite & ( for s being Element of PFuncs V',C' holds
( ( s in B & s c= t ) iff s = t ) ) ) } by SUBSTLAT:def 2;
then consider f being Element of PFuncs V',C' such that
A6: ( f = x & f is finite & ( for s being Element of PFuncs V',C' holds
( ( s in B & s c= f ) iff s = f ) ) ) ;
reconsider x' = x as finite set by A6;
A7: mi B c= B by SUBSTLAT:8;
for b being finite set st b in A & b c= x' holds
b = x' by A1, A5, SUBSTLAT:6;
hence x in mi A by A1, A5, A7, SUBSTLAT:7; :: thesis: verum