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 A4: ( ( 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.} ) ) ; :: thesis: IT1 = IT2

now

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

end;

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