let R be Element of n -tuples_on BOOLEAN; :: thesis: ( R = Op-XOR (t,) iff for i being Nat st i in Seg n holds
R . i = (s . i) 'xor' (t . i) )
set F = s 'xor' t;

A1: now :: thesis: for R being Element of n -tuples_on BOOLEAN holds dom R = Seg n

let R be Element of n -tuples_on BOOLEAN; :: thesis: dom R = Seg n
thus dom R = Seg (len R) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7 ; :: thesis: verum

end;

then A2: dom R = Seg n ;
hence ( R = s 'xor' t implies for i being Nat st i in Seg n holds
R . i = (s . i) 'xor' (t . i) ) by BVFUNC_1:def 3; :: thesis: ( ( for i being Nat st i in Seg n holds
R . i = (s . i) 'xor' (t . i) ) implies R = Op-XOR (t,) )
A3: ( dom s = Seg n & dom t = Seg n ) by A1;
A4: (Seg n) /\ (Seg n) = Seg n ;
assume for i being Nat st i in Seg n holds
R . i = (s . i) 'xor' (t . i) ; :: thesis: R = Op-XOR (t,)
then for x being set st x in dom R holds
R . x = (s . x) 'xor' (t . x) by A2;
hence R = s 'xor' t by A1, A3, A4, BVFUNC_1:def 3; :: thesis: verum