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

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:113; :: thesis: verum