let s, t be Function of 16,(4 -tuples_on BOOLEAN); :: thesis: ( s . 0 = <*0,0,0,0*> & s . 1 = <*0,0,0,1*> & s . 2 = <*0,0,1,0*> & s . 3 = <*0,0,1,1*> & s . 4 = <*0,1,0,0*> & s . 5 = <*0,1,0,1*> & s . 6 = <*0,1,1,0*> & s . 7 = <*0,1,1,1*> & s . 8 = <*1,0,0,0*> & s . 9 = <*1,0,0,1*> & s . 10 = <*1,0,1,0*> & s . 11 = <*1,0,1,1*> & s . 12 = <*1,1,0,0*> & s . 13 = <*1,1,0,1*> & s . 14 = <*1,1,1,0*> & s . 15 = <*1,1,1,1*> & t . 0 = <*0,0,0,0*> & t . 1 = <*0,0,0,1*> & t . 2 = <*0,0,1,0*> & t . 3 = <*0,0,1,1*> & t . 4 = <*0,1,0,0*> & t . 5 = <*0,1,0,1*> & t . 6 = <*0,1,1,0*> & t . 7 = <*0,1,1,1*> & t . 8 = <*1,0,0,0*> & t . 9 = <*1,0,0,1*> & t . 10 = <*1,0,1,0*> & t . 11 = <*1,0,1,1*> & t . 12 = <*1,1,0,0*> & t . 13 = <*1,1,0,1*> & t . 14 = <*1,1,1,0*> & t . 15 = <*1,1,1,1*> implies s = t )
assume AS1: ( s . 0 = <*0,0,0,0*> & s . 1 = <*0,0,0,1*> & s . 2 = <*0,0,1,0*> & s . 3 = <*0,0,1,1*> & s . 4 = <*0,1,0,0*> & s . 5 = <*0,1,0,1*> & s . 6 = <*0,1,1,0*> & s . 7 = <*0,1,1,1*> & s . 8 = <*1,0,0,0*> & s . 9 = <*1,0,0,1*> & s . 10 = <*1,0,1,0*> & s . 11 = <*1,0,1,1*> & s . 12 = <*1,1,0,0*> & s . 13 = <*1,1,0,1*> & s . 14 = <*1,1,1,0*> & s . 15 = <*1,1,1,1*> ) ; :: thesis: ( not t . 0 = <*0,0,0,0*> or not t . 1 = <*0,0,0,1*> or not t . 2 = <*0,0,1,0*> or not t . 3 = <*0,0,1,1*> or not t . 4 = <*0,1,0,0*> or not t . 5 = <*0,1,0,1*> or not t . 6 = <*0,1,1,0*> or not t . 7 = <*0,1,1,1*> or not t . 8 = <*1,0,0,0*> or not t . 9 = <*1,0,0,1*> or not t . 10 = <*1,0,1,0*> or not t . 11 = <*1,0,1,1*> or not t . 12 = <*1,1,0,0*> or not t . 13 = <*1,1,0,1*> or not t . 14 = <*1,1,1,0*> or not t . 15 = <*1,1,1,1*> or s = t )
L1: dom s = 16 by FUNCT_2:def 1;
assume AS2: ( t . 0 = <*0,0,0,0*> & t . 1 = <*0,0,0,1*> & t . 2 = <*0,0,1,0*> & t . 3 = <*0,0,1,1*> & t . 4 = <*0,1,0,0*> & t . 5 = <*0,1,0,1*> & t . 6 = <*0,1,1,0*> & t . 7 = <*0,1,1,1*> & t . 8 = <*1,0,0,0*> & t . 9 = <*1,0,0,1*> & t . 10 = <*1,0,1,0*> & t . 11 = <*1,0,1,1*> & t . 12 = <*1,1,0,0*> & t . 13 = <*1,1,0,1*> & t . 14 = <*1,1,1,0*> & t . 15 = <*1,1,1,1*> ) ; :: thesis: s = t
L2: dom s = dom t by L1, FUNCT_2:def 1;
for i being set st i in dom s holds
s . i = t . i

proof

let i be set ; :: thesis: ( i in dom s implies s . i = t . i )
assume i in dom s ; :: thesis: s . i = t . i
then ( i = 0 or i = 1 or i = 2 or i = 3 or i = 4 or i = 5 or i = 6 or i = 7 or i = 8 or i = 9 or i = 10 or i = 11 or i = 12 or i = 13 or i = 14 or i = 15 ) by thel16;
hence s . i = t . i by AS1, AS2; :: thesis: verum

end;

hence s = t by L2, FUNCT_1:2; :: thesis: verum