let f, g be Function of Q,Q; :: thesis: ( ( for u being Element of Q holds f . u = L_map (u,x,y) ) & ( for u being Element of Q holds g . u = L_map (u,x,y) ) implies f = g )
assume that
A1: for u being Element of Q holds f . u = H₁(u) and
A2: for u being Element of Q holds g . u = H₁(u) ; :: thesis: f = g
let u be Element of Q; :: according to FUNCT_2:def 8 :: thesis: f . u = g . u
thus f . u = H₁(u) by A1
.= g . u by A2 ; :: thesis: verum