let V, V9, C, C9 be set ; :: thesis: for A being Element of Fin (PFuncs (V,C))
for B being Element of Fin (PFuncs (V9,C9)) st V c= V9 & C c= C9 & A = B holds
mi A = mi B
let A be Element of Fin (PFuncs (V,C)); :: thesis: for B being Element of Fin (PFuncs (V9,C9)) st V c= V9 & C c= C9 & A = B holds
mi A = mi B
let B be Element of Fin (PFuncs (V9,C9)); :: thesis: ( V c= V9 & C c= C9 & A = B implies mi A = mi B )
assume that
A1: ( V c= V9 & C c= C9 ) and
A2: 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 object ; :: thesis: ( x in mi A implies x in mi B )
A3: PFuncs (V,C) c= PFuncs (V9,C9) by A1, PARTFUN1:50;
assume A4: 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
A5: f = x and
A6: f is finite and
for s being Element of PFuncs (V,C) holds
( ( s in A & s c= f ) iff s = f ) ;
reconsider f = f as Element of PFuncs (V9,C9) by A3;
for s being Element of PFuncs (V9,C9) holds
( ( s in B & s c= f ) iff s = f ) by A2, A4, A5, SUBSTLAT:6;
then x in { t where t is Element of PFuncs (V9,C9) : ( t is finite & ( for s being Element of PFuncs (V9,C9) holds
( ( s in B & s c= t ) iff s = t ) ) ) } by A5, A6;
hence x in mi B by SUBSTLAT:def 2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in mi B or x in mi A )
assume A7: x in mi B ; :: thesis: x in mi A
then x in { t where t is Element of PFuncs (V9,C9) : ( t is finite & ( for s being Element of PFuncs (V9,C9) holds
( ( s in B & s c= t ) iff s = t ) ) ) } by SUBSTLAT:def 2;
then ex f being Element of PFuncs (V9,C9) st
( f = x & f is finite & ( for s being Element of PFuncs (V9,C9) holds
( ( s in B & s c= f ) iff s = f ) ) ) ;
then reconsider x9 = x as finite set ;
( mi B c= B & ( for b being finite set st b in A & b c= x9 holds
b = x9 ) ) by A2, A7, SUBSTLAT:6;
hence x in mi A by A2, A7, SUBSTLAT:7; :: thesis: verum