let C1, C2 be Function of X,NAT; :: thesis: ( ( for a being object holds
( not a in X or ( ex n being Nat st a in B . n & a in B . (C1 . a) ) or ( ( for n being Nat holds not a in B . n ) & C1 . a = 0 ) ) ) & ( for a being object holds
( not a in X or ( ex n being Nat st a in B . n & a in B . (C2 . a) ) or ( ( for n being Nat holds not a in B . n ) & C2 . a = 0 ) ) ) implies C1 = C2 )
assume that
A1: for a being object holds
( not a in X or ( ex n being Nat st a in B . n & a in B . (C1 . a) ) or ( ( for n being Nat holds not a in B . n ) & C1 . a = 0 ) ) and
A2: for a being object holds
( not a in X or ( ex n being Nat st a in B . n & a in B . (C2 . a) ) or ( ( for n being Nat holds not a in B . n ) & C2 . a = 0 ) ) ; :: thesis: C1 = C2
A4: dom C1 = X by FUNCT_2:def 1;
A5: dom C1 = dom C2 by FUNCT_2:def 1, A4;
for a being object st a in X holds
C1 . a = C2 . a

proof

let a be object ; :: thesis: ( a in X implies C1 . a = C2 . a )
assume A6: a in X ; :: thesis: C1 . a = C2 . a

per cases ( ex n being Nat st a in B . n or for n being Nat holds not a in B . n ) ;

suppose A11: ex n being Nat st a in B . n ; :: thesis: C1 . a = C2 . a

then A12: a in B . (C1 . a) by A1, A6;
a in B . (C2 . a) by A2, A6, A11;
hence C1 . a = C2 . a by A12, Th29; :: thesis: verum

end;

suppose A20: for n being Nat holds not a in B . n ; :: thesis: C1 . a = C2 . a

then C1 . a = 0 by A1, A6
.= C2 . a by A2, A6, A20 ;
hence C1 . a = C2 . a ; :: thesis: verum

end;

end;

end;

hence C1 = C2 by A4, A5, FUNCT_1:def 11; :: thesis: verum