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

dom f = the carrier of L by FUNCT_2:def 1;

hence f = g by A7, A6, FUNCT_1:2; :: thesis: verum

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

A7:
dom g = the carrier of L
by FUNCT_2:def 1;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;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

dom f = the carrier of L by FUNCT_2:def 1;

hence f = g by A7, A6, FUNCT_1:2; :: thesis: verum