set x = q `1 ;
set y = q `2 ;
set a = q `3 ;
set b = q `4 ;
let f1, f2 be BiFunction of (new_set A),L; :: thesis: ( ( 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 & f1 . {{{A}}},{{A}} = q `3 & f1 . {A},{{A}} = q `4 & f1 . {{A}},{A} = q `4 & f1 . {A},{{{A}}} = (q `3 ) "\/" (q `4 ) & f1 . {{{A}}},{A} = (q `3 ) "\/" (q `4 ) & ( for u being Element of A holds
( f1 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & f1 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & f1 . u,{{A}} = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & f1 . {{A}},u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & f1 . u,{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) & f1 . {{{A}}},u = (d . u,(q `2 )) "\/" (q `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 & f2 . {{{A}}},{{A}} = q `3 & f2 . {A},{{A}} = q `4 & f2 . {{A}},{A} = q `4 & f2 . {A},{{{A}}} = (q `3 ) "\/" (q `4 ) & f2 . {{{A}}},{A} = (q `3 ) "\/" (q `4 ) & ( for u being Element of A holds
( f2 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & f2 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & f2 . u,{{A}} = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & f2 . {{A}},u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & f2 . u,{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) & f2 . {{{A}}},u = (d . u,(q `2 )) "\/" (q `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 and
A34: f1 . {{{A}}},{{A}} = q `3 and
A35: f1 . {A},{{A}} = q `4 and
A36: f1 . {{A}},{A} = q `4 and
A37: f1 . {A},{{{A}}} = (q `3 ) "\/" (q `4 ) and
A38: f1 . {{{A}}},{A} = (q `3 ) "\/" (q `4 ) and
A39: for u being Element of A holds
( f1 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & f1 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & f1 . u,{{A}} = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & f1 . {{A}},u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & f1 . u,{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) & f1 . {{{A}}},u = (d . u,(q `2 )) "\/" (q `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 and
A45: f2 . {{{A}}},{{A}} = q `3 and
A46: f2 . {A},{{A}} = q `4 and
A47: f2 . {{A}},{A} = q `4 and
A48: f2 . {A},{{{A}}} = (q `3 ) "\/" (q `4 ) and
A49: f2 . {{{A}}},{A} = (q `3 ) "\/" (q `4 ) and
A50: for u being Element of A holds
( f2 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & f2 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & f2 . u,{{A}} = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & f2 . {{A}},u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & f2 . u,{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) & f2 . {{{A}}},u = (d . u,(q `2 )) "\/" (q `4 ) ) ; :: thesis: f1 = f2

now

let p, q be Element of new_set A; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂
A51: ( p in A or p in {{A},{{A}},{{{A}}}} ) by XBOOLE_0:def 3;
A52: ( q in A or q in {{A},{{A}},{{{A}}}} ) by XBOOLE_0:def 3;

per cases ( ( p in A & q in A ) or ( p in A & q = {A} ) or ( p in A & q = {{A}} ) or ( p in A & q = {{{A}}} ) or ( p = {A} & q in A ) or ( p = {A} & q = {A} ) or ( p = {A} & q = {{A}} ) or ( p = {A} & q = {{{A}}} ) or ( p = {{A}} & q in A ) or ( p = {{A}} & q = {A} ) or ( p = {{A}} & q = {{A}} ) or ( p = {{A}} & q = {{{A}}} ) or ( p = {{{A}}} & q in A ) or ( p = {{{A}}} & q = {A} ) or ( p = {{{A}}} & q = {{A}} ) or ( p = {{{A}}} & q = {{{A}}} ) ) by A51, A52, ENUMSET1:def 1;

suppose A53: ( p in A & q in A ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = d . p,q by A29
.= f2 . p,q by A40, A53 ;
:: thesis: verum

end;

suppose A54: ( p in A & q = {A} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

then reconsider p9 = p as Element of A ;
thus f1 . p,q = (d . p9,(q `1 )) "\/" (q `3 ) by A39, A54
.= f2 . p,q by A50, A54 ; :: thesis: verum

end;

suppose A55: ( p in A & q = {{A}} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

then reconsider p9 = p as Element of A ;
thus f1 . p,q = ((d . p9,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) by A39, A55
.= f2 . p,q by A50, A55 ; :: thesis: verum

end;

suppose A56: ( p in A & q = {{{A}}} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

then reconsider p9 = p as Element of A ;
thus f1 . p,q = (d . p9,(q `2 )) "\/" (q `4 ) by A39, A56
.= f2 . p,q by A50, A56 ; :: thesis: verum

end;

suppose A57: ( p = {A} & q in A ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

then reconsider q9 = q as Element of A ;
thus f1 . p,q = (d . q9,(q `1 )) "\/" (q `3 ) by A39, A57
.= f2 . p,q by A50, A57 ; :: thesis: verum

end;

suppose ( p = {A} & q = {A} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = f2 . p,q by A30, A41; :: thesis: verum

end;

suppose ( p = {A} & q = {{A}} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = f2 . p,q by A35, A46; :: thesis: verum

end;

suppose ( p = {A} & q = {{{A}}} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = f2 . p,q by A37, A48; :: thesis: verum

end;

suppose A58: ( p = {{A}} & q in A ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

then reconsider q9 = q as Element of A ;
thus f1 . p,q = ((d . q9,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) by A39, A58
.= f2 . p,q by A50, A58 ; :: thesis: verum

end;

suppose ( p = {{A}} & q = {A} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = f2 . p,q by A36, A47; :: thesis: verum

end;

suppose ( p = {{A}} & q = {{A}} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = f2 . p,q by A31, A42; :: thesis: verum

end;

suppose ( p = {{A}} & q = {{{A}}} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = f2 . p,q by A33, A44; :: thesis: verum

end;

suppose A59: ( p = {{{A}}} & q in A ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

then reconsider q9 = q as Element of A ;
thus f1 . p,q = (d . q9,(q `2 )) "\/" (q `4 ) by A39, A59
.= f2 . p,q by A50, A59 ; :: thesis: verum

end;

suppose ( p = {{{A}}} & q = {A} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = f2 . p,q by A38, A49; :: thesis: verum

end;

suppose ( p = {{{A}}} & q = {{A}} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = f2 . p,q by A34, A45; :: thesis: verum

end;

suppose ( p = {{{A}}} & q = {{{A}}} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = f2 . p,q by A32, A43; :: thesis: verum

end;

end;

end;

hence f1 = f2 by BINOP_1:2; :: thesis: verum