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; :: 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_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) ) ; :: thesis: f1 = f2

now :: thesis: for p, q being Element of new_set A holds f1 . (p,q) = f2 . (p,q)

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_4))) "\/" (q `3_4) 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_4))) "\/" (q `3_4)) "\/" (q `4_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_4))) "\/" (q `4_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_4))) "\/" (q `3_4) 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_4))) "\/" (q `3_4)) "\/" (q `4_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_4))) "\/" (q `4_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 ; :: thesis: verum