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

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

hence
F1 = F2
by FUNCT_2:63; :: thesis: verumlet 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;thus F1 . x = f .: [:(x `1),(x `2):] by A1

.= F2 . x by A2 ; :: thesis: verum