let f1, f2 be Function of [: the carrier of Z_2,(n -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN); :: thesis: ( ( for a being Element of BOOLEAN
for x being Element of n -tuples_on BOOLEAN
for i being set st i in Seg n holds
(f1 . (a,x)) . i = a '&' (x . i) ) & ( for a being Element of BOOLEAN
for x being Element of n -tuples_on BOOLEAN
for i being set st i in Seg n holds
(f2 . (a,x)) . i = a '&' (x . i) ) implies f1 = f2 )
assume A7: for a being Element of BOOLEAN
for x being Element of n -tuples_on BOOLEAN
for i being set st i in Seg n holds
(f1 . (a,x)) . i = a '&' (x . i) ; :: thesis: ( ex a being Element of BOOLEAN ex x being Element of n -tuples_on BOOLEAN ex i being set st
( i in Seg n & not (f2 . (a,x)) . i = a '&' (x . i) ) or f1 = f2 )
assume A8: for a being Element of BOOLEAN
for x being Element of n -tuples_on BOOLEAN
for i being set st i in Seg n holds
(f2 . (a,x)) . i = a '&' (x . i) ; :: thesis: f1 = f2

now :: thesis: for a being Element of the carrier of Z_2
for x being Element of n -tuples_on BOOLEAN holds f1 . (a,x) = f2 . (a,x)

let a be Element of the carrier of Z_2; :: thesis: for x being Element of n -tuples_on BOOLEAN holds f1 . (a,x) = f2 . (a,x)
let x be Element of n -tuples_on BOOLEAN; :: thesis: f1 . (a,x) = f2 . (a,x)
A9: len (f1 . (a,x)) = n by CARD_1:def 7;
A10: len (f2 . (a,x)) = n by CARD_1:def 7;

now :: thesis: for i being Nat st 1 <= i & i <= len (f1 . (a,x)) holds
(f1 . (a,x)) . i = (f2 . (a,x)) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len (f1 . (a,x)) implies (f1 . (a,x)) . i = (f2 . (a,x)) . i )
assume ( 1 <= i & i <= len (f1 . (a,x)) ) ; :: thesis: (f1 . (a,x)) . i = (f2 . (a,x)) . i
then A11: i in Seg n by A9;
thus (f1 . (a,x)) . i = a '&' (x . i) by A7, A11, BSPACE:3
.= (f2 . (a,x)) . i by A8, A11, BSPACE:3 ; :: thesis: verum

end;

hence f1 . (a,x) = f2 . (a,x) by FINSEQ_1:14, CARD_1:def 7, A10; :: thesis: verum

end;

hence f1 = f2 by BINOP_1:2; :: thesis: verum