let E be non empty set ; :: thesis: for v1, v2, w1, w2 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 v1, v2, w1, w2 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 )
A3: (len w1) + (len v1) = len (w2 ^ v2) by A1, AFINSQ_1:17
.= (len w2) + (len v2) by AFINSQ_1:17 ;

now :: thesis: for k being Nat st k in dom w1 holds
w1 . k = w2 . k

let k be Nat; :: thesis: ( k in dom w1 implies w1 . k = w2 . k )
assume A4: k in dom w1 ; :: thesis: w1 . k = w2 . k
hence w1 . k = (w2 ^ v2) . k by A1, AFINSQ_1:def 3
.= w2 . k by A2, A3, A4, AFINSQ_1:def 3 ;
:: thesis: verum

end;

hence w1 = w2 by A2, A3, AFINSQ_1:8; :: thesis: v1 = v2
hence v1 = v2 by A1, AFINSQ_1:28; :: thesis: verum