let f1, f2 be Function of (bool X),(bool X); :: thesis: ( ( for x being Subset of X holds f1 . x = (f . (x `)) ` ) & ( for x being Subset of X holds f2 . x = (f . (x `)) ` ) implies f1 = f2 )
assume that
A2: for x being Subset of X holds f1 . x = (f . (x `)) ` and
A3: for x being Subset of X holds f2 . x = (f . (x `)) ` ; :: thesis: f1 = f2
let x be Subset of X; :: according to FUNCT_2:def 8 :: thesis: f1 . x = f2 . x
thus f1 . x = (f . (x `)) ` by A2
.= f2 . x by A3 ; :: thesis: verum