now :: thesis: for IT1, IT2 being Function of E,E st ex PF1 being FinSequence of Funcs (E,E) st
( IT1 = PF1 . (len F) & len PF1 = len F & PF1 . 1 = A . (F . 1) & ( for k being Nat st k <> 0 & k < len F holds
ex f, g being Function of E,E st
( f = PF1 . k & g = A . (F . (k + 1)) & PF1 . (k + 1) = f * g ) ) ) & ex PF2 being FinSequence of Funcs (E,E) st
( IT2 = PF2 . (len F) & len PF2 = len F & PF2 . 1 = A . (F . 1) & ( for k being Nat st k <> 0 & k < len F holds
ex f, g being Function of E,E st
( f = PF2 . k & g = A . (F . (k + 1)) & PF2 . (k + 1) = f * g ) ) ) holds
IT1 = IT2
let IT1, IT2 be Function of E,E; :: thesis: ( ex PF1 being FinSequence of Funcs (E,E) st
( IT1 = PF1 . (len F) & len PF1 = len F & PF1 . 1 = A . (F . 1) & ( for k being Nat st k <> 0 & k < len F holds
ex f, g being Function of E,E st
( f = PF1 . k & g = A . (F . (k + 1)) & PF1 . (k + 1) = f * g ) ) ) & ex PF2 being FinSequence of Funcs (E,E) st
( IT2 = PF2 . (len F) & len PF2 = len F & PF2 . 1 = A . (F . 1) & ( for k being Nat st k <> 0 & k < len F holds
ex f, g being Function of E,E st
( f = PF2 . k & g = A . (F . (k + 1)) & PF2 . (k + 1) = f * g ) ) ) implies IT1 = IT2 )

given PF1 being FinSequence of Funcs (E,E) such that A32: IT1 = PF1 . (len F) and
A33: len PF1 = len F and
A34: PF1 . 1 = A . (F . 1) and
A35: for k being Nat st k <> 0 & k < len F holds
ex f, g being Function of E,E st
( f = PF1 . k & g = A . (F . (k + 1)) & PF1 . (k + 1) = f * g ) ; :: thesis: ( ex PF2 being FinSequence of Funcs (E,E) st
( IT2 = PF2 . (len F) & len PF2 = len F & PF2 . 1 = A . (F . 1) & ( for k being Nat st k <> 0 & k < len F holds
ex f, g being Function of E,E st
( f = PF2 . k & g = A . (F . (k + 1)) & PF2 . (k + 1) = f * g ) ) ) implies IT1 = IT2 )

given PF2 being FinSequence of Funcs (E,E) such that A36: ( IT2 = PF2 . (len F) & len PF2 = len F ) and
A37: PF2 . 1 = A . (F . 1) and
A38: for k being Nat st k <> 0 & k < len F holds
ex f, g being Function of E,E st
( f = PF2 . k & g = A . (F . (k + 1)) & PF2 . (k + 1) = f * g ) ; :: thesis: IT1 = IT2
defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= len PF1 implies PF1 . \$1 = PF2 . \$1 );
A39: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A40: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( 1 <= k + 1 & k + 1 <= len PF1 implies PF1 . (k + 1) = PF2 . (k + 1) )
assume 1 <= k + 1 ; :: thesis: ( k + 1 <= len PF1 implies PF1 . (k + 1) = PF2 . (k + 1) )
assume A41: k + 1 <= len PF1 ; :: thesis: PF1 . (k + 1) = PF2 . (k + 1)
then A42: k < len PF1 by NAT_1:13;
per cases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; :: thesis: PF1 . (k + 1) = PF2 . (k + 1)
hence PF1 . (k + 1) = PF2 . (k + 1) by ; :: thesis: verum
end;
suppose A43: k <> 0 ; :: thesis: PF1 . (k + 1) = PF2 . (k + 1)
then A44: 0 + 1 < k + 1 by XREAL_1:6;
( ex f1, g1 being Function of E,E st
( f1 = PF1 . k & g1 = A . (F . (k + 1)) & PF1 . (k + 1) = f1 * g1 ) & ex f2, g2 being Function of E,E st
( f2 = PF2 . k & g2 = A . (F . (k + 1)) & PF2 . (k + 1) = f2 * g2 ) ) by A33, A35, A38, A42, A43;
hence PF1 . (k + 1) = PF2 . (k + 1) by ; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A45: S1[ 0 ] ;
for k being Nat holds S1[k] from hence IT1 = IT2 by ; :: thesis: verum
end;
hence for b1, b2 being Function of E,E holds
( ( len F = 0 & b1 = id E & b2 = id E implies b1 = b2 ) & ( not len F = 0 & ex PF being FinSequence of Funcs (E,E) st
( b1 = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds
ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) & ex PF being FinSequence of Funcs (E,E) st
( b2 = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds
ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) implies b1 = b2 ) ) ; :: thesis: verum