set x = q `1_4 ;
set y = q `2_4 ;
set a = q `3_4 ;
set b = q `4_4 ;
let f1, f2 be BiFunction of (new_set 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}}}) = Bottom L & f1 . ({{A}},{{{A}}}) = q `3_4 & f1 . ({{{A}}},{{A}}) = q `3_4 & f1 . ({A},{{A}}) = q `4_4 & f1 . ({{A}},{A}) = q `4_4 & f1 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & f1 . ({{{A}}},{A}) = (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 `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f1 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f1 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & f1 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_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}}}) = Bottom L & f2 . ({{A}},{{{A}}}) = q `3_4 & f2 . ({{{A}}},{{A}}) = q `3_4 & f2 . ({A},{{A}}) = q `4_4 & f2 . ({{A}},{A}) = q `4_4 & f2 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & f2 . ({{{A}}},{A}) = (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 `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f2 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f2 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & f2 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) implies f1 = f2 )
assume that
A29:
for u, v being Element of A holds f1 . (u,v) = d . (u,v)
and
A30:
f1 . ({A},{A}) = Bottom L
and
A31:
f1 . ({{A}},{{A}}) = Bottom L
and
A32:
f1 . ({{{A}}},{{{A}}}) = Bottom L
and
A33:
f1 . ({{A}},{{{A}}}) = q `3_4
and
A34:
f1 . ({{{A}}},{{A}}) = q `3_4
and
A35:
f1 . ({A},{{A}}) = q `4_4
and
A36:
f1 . ({{A}},{A}) = q `4_4
and
A37:
f1 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4)
and
A38:
f1 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4)
and
A39:
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 `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f1 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f1 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & f1 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) )
and
A40:
for u, v being Element of A holds f2 . (u,v) = d . (u,v)
and
A41:
f2 . ({A},{A}) = Bottom L
and
A42:
f2 . ({{A}},{{A}}) = Bottom L
and
A43:
f2 . ({{{A}}},{{{A}}}) = Bottom L
and
A44:
f2 . ({{A}},{{{A}}}) = q `3_4
and
A45:
f2 . ({{{A}}},{{A}}) = q `3_4
and
A46:
f2 . ({A},{{A}}) = q `4_4
and
A47:
f2 . ({{A}},{A}) = q `4_4
and
A48:
f2 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4)
and
A49:
f2 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4)
and
A50:
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 `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f2 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f2 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & f2 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) )
; f1 = f2
hence
f1 = f2
; verum