let F1, F2 be Function of [:(bool D1),(bool D2):],(bool D); :: thesis: ( ( for x being Element of [:(bool D1),(bool D2):] holds F1 . x = f .: [:(x `1),(x `2):] ) & ( for x being Element of [:(bool D1),(bool D2):] holds F2 . x = f .: [:(x `1),(x `2):] ) implies F1 = F2 )
assume that
A1: for x being Element of [:(bool D1),(bool D2):] holds F1 . x = f .: [:(x `1),(x `2):] and
A2: for x being Element of [:(bool D1),(bool D2):] holds F2 . x = f .: [:(x `1),(x `2):] ; :: thesis: F1 = F2

now :: thesis: for x being Element of [:(bool D1),(bool D2):] holds F1 . x = F2 . x

let x be Element of [:(bool D1),(bool D2):]; :: thesis: F1 . x = F2 . x
thus F1 . x = f .: [:(x `1),(x `2):] by A1
.= F2 . x by A2 ; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:63; :: thesis: verum