let f1, f2 be Function of (QuasiTypes C), the carrier of VarPoset; :: thesis: ( ( for T being quasi-type of C holds f1 . T = vars T ) & ( for T being quasi-type of C holds f2 . T = vars T ) implies f1 = f2 )
assume that
A1: for T being quasi-type of C holds f1 . T = vars T and
A2: for T being quasi-type of C holds f2 . T = vars T ; :: thesis: f1 = f2

now :: thesis: for T being Element of QuasiTypes C holds f1 . T = f2 . T

let T be Element of QuasiTypes C; :: thesis: f1 . T = f2 . T
reconsider t = T as quasi-type of C by Def43;
thus f1 . T = vars t by A1
.= f2 . T by A2 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum