set x = q `1_4 ;
set y = q `2_4 ;
set a = q `3_4 ;
let f1, f2 be BiFunction of (new_set2 A),L; ( ( for u, v being Element of A holds f1 . (u,v) = d . (u,v) ) & f1 . ({A},{A}) = Bottom L & f1 . ({{A}},{{A}}) = Bottom L & f1 . ({A},{{A}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & f1 . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & ( for u being Element of A holds
( f1 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & f1 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & f1 . (u,{{A}}) = (d . (u,(q `2_4))) "\/" (q `3_4) & f1 . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_4) ) ) & ( for u, v being Element of A holds f2 . (u,v) = d . (u,v) ) & f2 . ({A},{A}) = Bottom L & f2 . ({{A}},{{A}}) = Bottom L & f2 . ({A},{{A}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & f2 . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & ( for u being Element of A holds
( f2 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & f2 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & f2 . (u,{{A}}) = (d . (u,(q `2_4))) "\/" (q `3_4) & f2 . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_4) ) ) implies f1 = f2 )
assume that
A20:
for u, v being Element of A holds f1 . (u,v) = d . (u,v)
and
A21:
f1 . ({A},{A}) = Bottom L
and
A22:
f1 . ({{A}},{{A}}) = Bottom L
and
A23:
f1 . ({A},{{A}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4)
and
A24:
f1 . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4)
and
A25:
for u being Element of A holds
( f1 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & f1 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & f1 . (u,{{A}}) = (d . (u,(q `2_4))) "\/" (q `3_4) & f1 . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_4) )
and
A26:
for u, v being Element of A holds f2 . (u,v) = d . (u,v)
and
A27:
f2 . ({A},{A}) = Bottom L
and
A28:
f2 . ({{A}},{{A}}) = Bottom L
and
A29:
f2 . ({A},{{A}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4)
and
A30:
f2 . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4)
and
A31:
for u being Element of A holds
( f2 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & f2 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & f2 . (u,{{A}}) = (d . (u,(q `2_4))) "\/" (q `3_4) & f2 . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_4) )
; f1 = f2
hence
f1 = f2
; verum