let p, q be XFinSequence; :: thesis: ( ( for k11, k21 being Element of NAT st k11 = k1 & k21 = k2 holds
p = (f | k21) /^ (k11 -' 1) ) & ( for k11, k21 being Element of NAT st k11 = k1 & k21 = k2 holds
q = (f | k21) /^ (k11 -' 1) ) implies p = q )
assume B1: ( ( for k11, k21 being Element of NAT st k11 = k1 & k21 = k2 holds
p = (f | k21) /^ (k11 -' 1) ) & ( for k11, k21 being Element of NAT st k11 = k1 & k21 = k2 holds
q = (f | k21) /^ (k11 -' 1) ) ) ; :: thesis: p = q
reconsider k12 = k1, k22 = k2 as Element of NAT by ORDINAL1:def 13;
p = (f | k22) /^ (k12 -' 1) by B1;
hence p = q by B1; :: thesis: verum