reconsider k12 = k1, k22 = k2 as Element of NAT by ORDINAL1:def 13;
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 that
A1: for k11, k21 being Element of NAT st k11 = k1 & k21 = k2 holds
p = (f | k21) /^ (k11 -' 1) and
A2: for k11, k21 being Element of NAT st k11 = k1 & k21 = k2 holds
q = (f | k21) /^ (k11 -' 1) ; :: thesis: p = q
p = (f | k22) /^ (k12 -' 1) by A1;
hence p = q by A2; :: thesis: verum