let f, g be Function of L,(InclPoset (Ids (subrelstr B))); :: thesis: ( ( for x being Element of L holds f . x = (waybelow x) /\ B ) & ( for x being Element of L holds g . x = (waybelow x) /\ B ) implies f = g )
assume that
A4: for x being Element of L holds f . x = (waybelow x) /\ B and
A5: for x being Element of L holds g . x = (waybelow x) /\ B ; :: thesis: f = g

A6: now :: thesis: for z being object st z in the carrier of L holds
f . z = g . z

let z be object ; :: thesis: ( z in the carrier of L implies f . z = g . z )
assume z in the carrier of L ; :: thesis: f . z = g . z
then reconsider z1 = z as Element of L ;
f . z = (waybelow z1) /\ B by A4;
hence f . z = g . z by A5; :: thesis: verum

end;

A7: dom g = the carrier of L by FUNCT_2:def 1;
dom f = the carrier of L by FUNCT_2:def 1;
hence f = g by A7, A6, FUNCT_1:2; :: thesis: verum