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; :: 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}}) = ((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) ) ; :: thesis: f1 = f2
now :: thesis: for p, q being Element of new_set2 A holds f1 . (p,q) = f2 . (p,q)
let p, q be Element of new_set2 A; :: thesis: f1 . (b1,b2) = f2 . (b1,b2)
A32: ( p in A or p in {{A},{{A}}} ) by XBOOLE_0:def 3;
A33: ( q in A or q in {{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 = {A} & q in 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}} ) ) by A32, A33, TARSKI:def 2;
suppose A34: ( p in A & q in A ) ; :: thesis: f1 . (b1,b2) = f2 . (b1,b2)
hence f1 . (p,q) = d . (p,q) by A20
.= f2 . (p,q) by A26, A34 ;
:: thesis: verum
end;
suppose A35: ( p in A & q = {A} ) ; :: thesis: f1 . (b1,b2) = f2 . (b1,b2)
then reconsider p9 = p as Element of A ;
thus f1 . (p,q) = (d . (p9,(q `1_4))) "\/" (q `3_4) by A25, A35
.= f2 . (p,q) by A31, A35 ; :: thesis: verum
end;
suppose A36: ( p in A & q = {{A}} ) ; :: thesis: f1 . (b1,b2) = f2 . (b1,b2)
then reconsider p9 = p as Element of A ;
thus f1 . (p,q) = (d . (p9,(q `2_4))) "\/" (q `3_4) by A25, A36
.= f2 . (p,q) by A31, A36 ; :: thesis: verum
end;
suppose A37: ( p = {A} & q in A ) ; :: thesis: f1 . (b1,b2) = f2 . (b1,b2)
then reconsider q9 = q as Element of A ;
thus f1 . (p,q) = (d . (q9,(q `1_4))) "\/" (q `3_4) by A25, A37
.= f2 . (p,q) by A31, A37 ; :: thesis: verum
end;
suppose ( p = {A} & q = {A} ) ; :: thesis: f1 . (b1,b2) = f2 . (b1,b2)
hence f1 . (p,q) = f2 . (p,q) by A21, A27; :: thesis: verum
end;
suppose ( p = {A} & q = {{A}} ) ; :: thesis: f1 . (b1,b2) = f2 . (b1,b2)
hence f1 . (p,q) = f2 . (p,q) by A23, A29; :: thesis: verum
end;
suppose A38: ( p = {{A}} & q in A ) ; :: thesis: f1 . (b1,b2) = f2 . (b1,b2)
then reconsider q9 = q as Element of A ;
thus f1 . (p,q) = (d . (q9,(q `2_4))) "\/" (q `3_4) by A25, A38
.= f2 . (p,q) by A31, A38 ; :: thesis: verum
end;
suppose ( p = {{A}} & q = {A} ) ; :: thesis: f1 . (b1,b2) = f2 . (b1,b2)
hence f1 . (p,q) = f2 . (p,q) by A24, A30; :: thesis: verum
end;
suppose ( p = {{A}} & q = {{A}} ) ; :: thesis: f1 . (b1,b2) = f2 . (b1,b2)
hence f1 . (p,q) = f2 . (p,q) by A22, A28; :: thesis: verum
end;
end;
end;
hence f1 = f2 ; :: thesis: verum