let h1, h2 be Function of the Lines of , the Lines of ; :: thesis: ( ( for x being LINE of holds h1 . x = { (() . P) where P is POINT of : P on x } ) & ( for x being LINE of holds h2 . x = { (() . P) where P is POINT of : P on x } ) implies h1 = h2 )
assume that
A14: for x being LINE of holds h1 . x = { (() . P) where P is POINT of : P on x } and
A15: for x being LINE of holds h2 . x = { (() . P) where P is POINT of : P on x } ; :: thesis: h1 = h2
now :: thesis: ( dom h1 = dom h2 & ( for x9 being object st x9 in dom h1 holds
h1 . x9 = h2 . x9 ) )
dom h1 = the Lines of by FUNCT_2:def 1;
hence dom h1 = dom h2 by FUNCT_2:def 1; :: thesis: for x9 being object st x9 in dom h1 holds
h1 . x9 = h2 . x9

hereby :: thesis: verum
let x9 be object ; :: thesis: ( x9 in dom h1 implies h1 . x9 = h2 . x9 )
assume x9 in dom h1 ; :: thesis: h1 . x9 = h2 . x9
then reconsider y = x9 as LINE of ;
h1 . y = { (() . P) where P is POINT of : P on y } by A14
.= h2 . y by A15 ;
hence h1 . x9 = h2 . x9 ; :: thesis: verum
end;
end;
hence h1 = h2 by FUNCT_1:def 11; :: thesis: verum