let E be non empty set ; :: thesis: for w1, v1, w2, v2 being Element of E ^omega st w1 ^ v1 = w2 ^ v2 & ( len w1 = len w2 or len v1 = len v2 ) holds
( w1 = w2 & v1 = v2 )
let w1, v1, w2, v2 be Element of E ^omega ; :: thesis: ( w1 ^ v1 = w2 ^ v2 & ( len w1 = len w2 or len v1 = len v2 ) implies ( w1 = w2 & v1 = v2 ) )
assume that
A1: w1 ^ v1 = w2 ^ v2 and
A2: ( len w1 = len w2 or len v1 = len v2 ) ; :: thesis: ( w1 = w2 & v1 = v2 )
B: (len w1) + (len v1) = len (w2 ^ v2) by A1, AFINSQ_1:20
.= (len w2) + (len v2) by AFINSQ_1:20 ;

now

let k be Element of NAT ; :: thesis: ( k in dom w1 implies w1 . k = w2 . k )
assume C: k in dom w1 ; :: thesis: w1 . k = w2 . k
hence w1 . k = (w2 ^ v2) . k by A1, AFINSQ_1:def 4
.= w2 . k by A2, B, C, AFINSQ_1:def 4 ;
:: thesis: verum

end;

hence w1 = w2 by A2, B, AFINSQ_1:10; :: thesis: v1 = v2
hence v1 = v2 by A1, AFINSQ_1:31; :: thesis: verum