let IT1, IT2 be Function of (PFuncs (V,C)), the carrier of (SubstLatt (V,C)); :: thesis: ( ( for a being Element of PFuncs (V,C) holds IT1 . a = mi {.a.} ) & ( for a being Element of PFuncs (V,C) holds IT2 . a = mi {.a.} ) implies IT1 = IT2 )
assume that
A4: for a being Element of PFuncs (V,C) holds IT1 . a = mi {.a.} and
A5: for a being Element of PFuncs (V,C) holds IT2 . a = mi {.a.} ; :: thesis: IT1 = IT2

now :: thesis: for a being Element of PFuncs (V,C) holds IT1 . a = IT2 . a

let a be Element of PFuncs (V,C); :: thesis: IT1 . a = IT2 . a
IT1 . a = mi {.a.} by A4;
hence IT1 . a = IT2 . a by A5; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_2:63; :: thesis: verum